Lean module · ETC
BanditRLProof.Algorithms.ETCExpectedPullCount
# ETC expected pull counts This module integrates the deterministic pull-count formula for an `Omega`-indexed ETC commit selector. It isolates the exact interface between ETC counting and concentration: a later tail argument only has to bound the commit-fiber probability `mu.real {omega | commit omega = a}`.
Module map
Imports
BanditRLProof.Algorithms.ETCTraceCountLemmas, BanditRLProof.MeasurablePullCountCast
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCExactSubGaussianTail, BanditRLProof.Algorithms.ETCRealEmpiricalMean
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ETC.integrable_real_pullCount_actionWithCommit_choice_of_measurable_commit
Compiled
The Real cast of a finite-horizon ETC pull count is integrable when the commit selector is measurable and the ambient measure is finite. This regularity adapter is independent of reward laws and concentration. Its proof uses timewise measurability of the finite-valued ETC action and the deterministic bound `pullCount <= n`.
theorem integrable_real_pullCount_actionWithCommit_choice_of_measurable_commit {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsFiniteMeasure mu] (spec : ETC.Spec K) (commit : Omega -> Fin K) (a : Fin K) (n : Nat) (hmeas_commit : Measurable commit) : Integrable (fun omega : Omega => ((pullCount (ETC.actionWithCommit spec (commit omega)) a n : Nat) : Real)) mu
theorem
BanditRLProof.ETC.integral_real_pullCount_actionWithCommit_choice_eq_exploration_add_suffix_mul_commit_prob
Compiled
At horizon `spec.explorationPulls * K + r`, the expected Real pull count of arm `a` is exactly the exploration count plus `r` times the probability of committing to `a`. This is the direct Bochner/indicator integration of `ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq`.
theorem integral_real_pullCount_actionWithCommit_choice_eq_exploration_add_suffix_mul_commit_prob {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (spec : ETC.Spec K) (commit : Omega -> Fin K) (a : Fin K) (r : Nat) (hmeas_commit : Measurable commit) : MeasureTheory.integral mu (fun omega : Omega => ((pullCount (ETC.actionWithCommit spec (commit omega)) a (spec.explorationPulls * K + r) : Nat) : Real)) = (spec.explorationPulls : Real) + (r : Real) * mu.real {omega : Omega | commit omega = a}
theorem
BanditRLProof.ETC.integral_real_pullCount_actionWithCommit_choice_eq_exploration_add_remaining_mul_commit_prob
Compiled
LML-shaped horizon form of the exact ETC expected pull-count identity. The exploration condition is written as `K * explorationPulls <= n`, and the suffix is `n - K * explorationPulls`, matching the exact ETC theorem-card surface. No concentration or reward-law assumption is used.
theorem integral_real_pullCount_actionWithCommit_choice_eq_exploration_add_remaining_mul_commit_prob {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (spec : ETC.Spec K) (commit : Omega -> Fin K) (a : Fin K) (n : Nat) (hn : K * spec.explorationPulls <= n) (hmeas_commit : Measurable commit) : MeasureTheory.integral mu (fun omega : Omega => ((pullCount (ETC.actionWithCommit spec (commit omega)) a n : Nat) : Real)) = (spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * mu.real {omega : Omega | commit omega = a}
theorem
BanditRLProof.ETC.integral_real_pullCount_actionWithCommit_choice_le_exploration_add_remaining_mul_of_commit_prob_le
Compiled
Per-arm ETC expected pull-count bound from a commit-fiber probability bound. This is the concentration consumer needed by the exact LML route: a later empirical-mean tail theorem supplies only `mu.real {omega | commit omega = a} <= p`; the counting and integration steps are discharged here.
theorem integral_real_pullCount_actionWithCommit_choice_le_exploration_add_remaining_mul_of_commit_prob_le {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (spec : ETC.Spec K) (commit : Omega -> Fin K) (a : Fin K) (n : Nat) (p : Real) (hn : K * spec.explorationPulls <= n) (hmeas_commit : Measurable commit) (hprob : mu.real {omega : Omega | commit omega = a} <= p) : MeasureTheory.integral mu (fun omega : Omega => ((pullCount (ETC.actionWithCommit spec (commit omega)) a n : Nat) : Real)) <= (spec.explorationPulls : Real) + ((n - K * spec.explorationPulls : Nat) : Real) * p