LF1 Main Theorem

Category: 3-Local (LF1 headline theorem: deterministic repeated-trial frequency convergence).

Glossary: https://glossary.constraintsurfacedynamics.com/lf1-main-theorem/ Plain-language, CSD-role and formal statements of the LF1 main theorem, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The theorem proved here is a deterministic repeated-trial typicality theorem. The ontic flow and outcome assignment are deterministic. Probability enters only through the repeated-preparation model on initial conditions. The convergence step then follows from a law of large numbers applied to the induced indicator observables.

Relation to the manuscript's partition language

The manuscript states the frequency theorem for a full measurable outcome partition {Ω_i^Σ}. The theorem here is stated for a single O : OutcomeRegion — one element of that partition — rather than for a formalised partition family object.

This is sufficient: the joint almost-sure statement for a finite partition follows by applying LF1_main_theorem_ae once per partition element and intersecting the resulting full-measure sets. A finite intersection of full-measure sets remains full-measure, so no additional structure is required at this layer.

See Outcomes.lean for further discussion of when a formalised partition type would become necessary (LF2/LF4 and POVM completeness).

theorem CSD.LF1.OnticSetup.TrialModel.main_theorem_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)

LF1 main theorem, real-valued version.

For a fixed measurable outcome region O, if the indicator random variables attached to the repeated-trial model are pairwise independent, then the empirical frequencies converge almost surely to the corresponding real-valued ontic weight.

Integrability and identical distribution are automatic consequences of the model structure and need not be supplied by the caller.

theorem CSD.LF1.OnticSetup.TrialModel.main_theorem_ae_mean_form {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 (∫ (x : Ω), T.indicatorRV O 0 x ∂trialMeasure S T))

Equivalent statement written with the expectation of the indicator random variable as the limit. This is useful when citing the theorem in a probability-theoretic form.

theorem CSD.LF1.OnticSetup.TrialModel.expectation_eq_weight {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : ∫ (x : Ω), T.indicatorRV O n x ∂trialMeasure S T = O.weightReal

The expectation of the indicator random variable equals the real-valued ontic weight. This is the expectation-to-weight bridge isolated for separate citation.

theorem CSD.LF1.OnticSetup.TrialModel.expectation_constant_across_trials {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : ∫ (x : Ω), T.indicatorRV O n x ∂trialMeasure S T = ∫ (x : Ω), T.indicatorRV O 0 x ∂trialMeasure S T

All trial expectations agree, because every trial has the same preparation law.

theorem CSD.LF1.OnticSetup.LF1_main_theorem_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 (TrialModel.trialMeasure S T)) fun (n : ℕ) => T.indicatorRV O n)) : ∀ᵐ (ω : Ω) ∂TrialModel.trialMeasure S T, Filter.Tendsto (fun (n : ℕ) => T.empiricalFreq O n ω) Filter.atTop (nhds O.weightReal)

LF1 main theorem. For a fixed outcome region O, the empirical frequency of O over repeated trials converges almost surely to the real-valued normalised ontic weight O.weightReal.

The only caller-supplied hypothesis is pairwise independence of the trial indicator random variables. Integrability and identical distribution follow automatically from the TrialModel structure.

Top-level alias for TrialModel.main_theorem_ae matching the manuscript statement of Paper A.