Lean module · Foundations
BanditRLProof.RatMeasurability
# Rat measurability wrappers This module contains narrow measurability wrappers for the project's Rat-valued bandit quantities. It deliberately does not choose probability, filtration, or concentration assumptions.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCEmpiricalMeanMeasurability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.measurable_rat_div_const
Compiled
Division by a fixed rational is measurable on a measurable singleton Rat space. This is the `RAT-MEASURABLE-DIV-CONST-OF-MEASURABLE-SINGLETON` wrapper. It is kept separate from the ETC empirical-mean theorem so later leaves can decide whether to consume it or keep an explicit division contract.
theorem measurable_rat_div_const [MeasurableSpace Rat] [MeasurableSingletonClass Rat] (c : Rat) : Measurable (fun x : Rat => x / c)