LF1 Indicators

Category: 3-Local (LF1 indicator random variables and empirical-frequency definitions).

A trial in LF1 is ontically deterministic. A sampled initial microstate x : Ω evolves under the measurable flow and yields an outcome by membership in a measurable ontic outcome event. The indicator random variable does not represent intrinsic stochastic evolution. It is the pullback of a deterministic outcome event along the repeated-trial preparation model.

Thus the probabilistic layer in LF1 enters only through repeated preparation sampling, not through stochastic ontic dynamics.

noncomputable def CSD.LF1.OnticSetup.TrialModel.indicatorRV {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : Ω → ℝ

The indicator random variable for outcome region O on trial n.

Takes value 1 when the n-th sampled initial condition lies in the pullback event associated with O, and 0 otherwise.

Equations

• T.indicatorRV O n = (T.trialEvent O n).indicator fun (x : Ω) => 1

theorem CSD.LF1.OnticSetup.TrialModel.measurable_indicatorRV {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : Measurable (T.indicatorRV O n)

Measurability of the indicator random variable.

theorem CSD.LF1.OnticSetup.TrialModel.indicatorRV_of_mem {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) {ω : Ω} (hω : ω ∈ T.trialEvent O n) : T.indicatorRV O n ω = 1

The indicator random variable takes value 1 on the event.

theorem CSD.LF1.OnticSetup.TrialModel.indicatorRV_of_not_mem {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) {ω : Ω} (hω : ω ∉ T.trialEvent O n) : T.indicatorRV O n ω = 0

The indicator random variable takes value 0 off the event.

theorem CSD.LF1.OnticSetup.TrialModel.indicatorRV_nonneg {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) (ω : Ω) : 0 ≤ T.indicatorRV O n ω

Pointwise nonnegativity of the indicator random variable.

theorem CSD.LF1.OnticSetup.TrialModel.indicatorRV_le_one {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) (ω : Ω) : T.indicatorRV O n ω ≤ 1

Pointwise upper bound by 1.

theorem CSD.LF1.OnticSetup.TrialModel.norm_indicatorRV_le_one {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) (ω : Ω) : ‖T.indicatorRV O n ω‖ ≤ 1

The indicator random variable is bounded in absolute value by 1.

theorem CSD.LF1.OnticSetup.TrialModel.aestronglyMeasurable_indicatorRV {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (T.indicatorRV O n) ↑T.P

The indicator random variable is a.e. strongly measurable w.r.t. the trial measure.

noncomputable def CSD.LF1.OnticSetup.TrialModel.empiricalFreq {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (N : ℕ) : Ω → ℝ

The empirical average of the first N indicator variables for outcome O. This is the object whose almost sure convergence is studied in Convergence.lean.

Equations

• T.empiricalFreq O N ω = (∑ j ∈ Finset.range N, T.indicatorRV O j ω) / ↑N

theorem CSD.LF1.OnticSetup.TrialModel.indicatorRV_integrable {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : MeasureTheory.Integrable (T.indicatorRV O n) ↑T.P

The indicator random variable is integrable with respect to the trial measure.

This follows from boundedness: ‖indicatorRV O n ω‖ ≤ 1 and the fact that the trial measure ((T.P : ProbabilityMeasure Ω) : Measure Ω) is a finite (probability) measure. (The T.trialMeasure abbreviation for this coercion is introduced downstream in Expectation.lean.)

theorem CSD.LF1.OnticSetup.TrialModel.indicatorRV_identDistrib {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : ProbabilityTheory.IdentDistrib (T.indicatorRV O n) (T.indicatorRV O 0) ↑T.P ↑T.P

All indicator random variables for a fixed outcome region have the same distribution.

This follows from T.hLaw: every trial X n has the same law (prepMeasure), so the pushforward of the composed indicator through each X n is identical.