LF1 Convergence

Category: 3-Local (LF1 strong-law application: empirical frequencies converge to ontic weights).

theorem CSD.LF1.OnticSetup.TrialModel.strongLaw_indicator_to_mean_ae {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g (trialMeasure S T)) fun (n : ℕ) => T.indicatorRV O n)) : ∀ᵐ (ω : Ω) ∂trialMeasure S T, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, T.indicatorRV O i ω) / ↑n) Filter.atTop (nhds (∫ (x : Ω), T.indicatorRV O 0 x ∂trialMeasure S T))

Strong law for the indicator random variables attached to a fixed outcome region.

It shows that the empirical frequency converges almost surely to the expectation of the indicator random variable. The separate identification of that expectation with the ontic weight is handled below through integral_indicatorRV_eq_weightReal.

Integrability and identical distribution are derived automatically from the model; only pairwise independence must be supplied by the caller.

theorem CSD.LF1.OnticSetup.TrialModel.strongLaw_indicator_to_weight_ae {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g (trialMeasure S T)) fun (n : ℕ) => T.indicatorRV O n)) : ∀ᵐ (ω : Ω) ∂trialMeasure S T, Filter.Tendsto (fun (n : ℕ) => (∑ i ∈ Finset.range n, T.indicatorRV O i ω) / ↑n) Filter.atTop (nhds O.weightReal)

If the expectation of the indicator random variable has been identified with the ontic preparation weight, then the empirical frequency converges almost surely to that weight.

theorem CSD.LF1.OnticSetup.TrialModel.strongLaw_empiricalFreq_to_weight_ae {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g (trialMeasure S T)) fun (n : ℕ) => T.indicatorRV O n)) : ∀ᵐ (ω : Ω) ∂trialMeasure S T, Filter.Tendsto (fun (n : ℕ) => T.empiricalFreq O n ω) Filter.atTop (nhds O.weightReal)

Version of the previous theorem written using the empiricalFreq abbreviation from Indicators.lean.