LF1 Expectation

Category: 3-Local (LF1 expectation-to-weight bridge E[𝟙_O] = O.weightReal).

@[reducible, inline]

abbrev CSD.LF1.OnticSetup.TrialModel.trialMeasure {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) : MeasureTheory.Measure Ω

The probability measure on the external repeated-trial sample space.

Equations

• CSD.LF1.OnticSetup.TrialModel.trialMeasure S T = ↑T.P

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

The same weight computed from the n-th trial event.

Equations

• CSD.LF1.OnticSetup.TrialModel.trialProbReal S T O n = (T.trialProb O n).toReal

@[simp]

theorem CSD.LF1.OnticSetup.TrialModel.trialProbReal_eq_weightReal {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : trialProbReal S T O n = O.weightReal

theorem CSD.LF1.OnticSetup.TrialModel.integral_indicatorRV_eq_trialProbReal {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 ω ∂trialMeasure S T = trialProbReal S T O n

The expectation of the indicator random variable is the real-valued probability of the corresponding trial event.

This is the key bridge lemma for LF1.

theorem CSD.LF1.OnticSetup.TrialModel.integral_indicatorRV_eq_weightReal {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 ω ∂trialMeasure S T = O.weightReal

The expectation of the indicator random variable is the real-valued ontic weight.

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

All indicator expectations agree across trials, because each trial has the same law.