Lean module · Foundations
BanditRLProof.ExpectationBochnerSums
# Bochner expectation over finite sums Thin Mathlib-backed wrappers for finite-sum linearity of the Bochner integral. These are the expectation-level companion to `IntegrabilitySums`: each summand must be integrable, and then the integral of the finite sum is the finite sum of the integrals.
Module map
Imports
BanditRLProof.IntegrabilitySums
Imported by
BanditRLProof, BanditRLProof.Algorithms.ETCExpectedRegretAssembly, BanditRLProof.Algorithms.ThompsonBayesRegretDecomposition, BanditRLProof.Exp3PredictableMoments, BanditRLProof.ExpectationRegretPullCount, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretFinitePrefixCumulativeAverageRate, BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeExplicitDeterministicMomentExpectedAverageRealizedBehaviorRegret, BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency, BanditRLProof.RL.FiniteHorizonNaturalCausalGrowingWindowGridStoppingTimeL1AverageRealizedBehaviorRegretConsistency, BanditRLProof.RL.FiniteHorizonNaturalCausalPolynomialBaseGrowingRawWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency, BanditRLProof.RealMeanRegretPullCount, BanditRLProof.TsallisConjugatePotentialFiniteHorizon, BanditRLProof.TsallisFTRLExpectedStability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ExpectationBochnerSums.integral_finset_sum
Compiled
The Bochner integral distributes over a finite sum of integrable terms. This is the `EXP-FINITE-SUM` import wrapper. It is polymorphic in the Bochner codomain; bandit expected-regret applications typically instantiate `E := Real`.
theorem integral_finset_sum {Omega : Type u} [MeasurableSpace Omega] {Idx : Type v} {E : Type w} [NormedAddCommGroup E] [NormedSpace Real E] (mu : Measure Omega) (s : Finset Idx) (f : Idx -> Omega -> E) (hf : forall i, i ∈ s -> Integrable (f i) mu) : MeasureTheory.integral mu (fun omega : Omega => s.sum (fun i => f i omega)) = s.sum (fun i => MeasureTheory.integral mu (f i))
theorem
BanditRLProof.ExpectationBochnerSums.integral_univ_sum
Compiled
Finite-type specialization of `integral_finset_sum`. The statement exposes the common finite-arm `(Finset.univ : Finset Idx)` shape used by regret decompositions.
theorem integral_univ_sum {Omega : Type u} [MeasurableSpace Omega] {Idx : Type v} [Fintype Idx] {E : Type w} [NormedAddCommGroup E] [NormedSpace Real E] (mu : Measure Omega) (f : Idx -> Omega -> E) (hf : forall i : Idx, Integrable (f i) mu) : MeasureTheory.integral mu (fun omega : Omega => (Finset.univ : Finset Idx).sum (fun i => f i omega)) = (Finset.univ : Finset Idx).sum (fun i => MeasureTheory.integral mu (f i))