InfiniteFutureStationarity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Preservation of mass by conditioning on the entire future

The actual normalized restrictions supplied by the increasing finite-label conditionings preserve the original measure when integrated over samples. This is a local disintegration identity, before any gluing of root boxes.

theorem OAI.DukePrimeDegree.integral_infinite_label_conditional_probability line 25

Source documentation

Integrating the probability of a measurable set under the genuine whole-future conditional recovers its original mass.

theorem integral_infinite_label_conditional_probability
    (ρ : Measure (S × V)) [IsFiniteMeasure ρ]
    {k : ℕ → ℕ} (Q : ∀ n, S × V → Fin (k n)) (hQ : ∀ n, Measurable (Q n))
    (hmono : Monotone (fun n => transverseLabelSigma (Q n)))
    (hdec : ∀ z, Antitone (fun n => labelFiber (Q n) z))
    (hpos : ∀ᵐ z ∂ρ, ρ.condKernel z.1 (⋂ n, labelFiber (Q n) z) ≠ 0)
    (A : Set (S × V)) (hA : MeasurableSet A) :
    let f := fun z =>
…

Mentions: OAI.DukePrimeDegree.transverseLabelSigma, OAI.DukePrimeDegree.labelFiber

theorem OAI.DukePrimeDegree.setIntegral_infinite_label_conditional_probability line 56

Source documentation

The disintegration identity remains valid on any event determined by the whole future and the transverse coordinate. This is the local restriction identity needed when gluing boxes along future events.

theorem setIntegral_infinite_label_conditional_probability
    (ρ : Measure (S × V)) [IsFiniteMeasure ρ]
    {k : ℕ → ℕ} (Q : ∀ n, S × V → Fin (k n)) (hQ : ∀ n, Measurable (Q n))
    (hmono : Monotone (fun n => transverseLabelSigma (Q n)))
    (hdec : ∀ z, Antitone (fun n => labelFiber (Q n) z))
    (hpos : ∀ᵐ z ∂ρ, ρ.condKernel z.1 (⋂ n, labelFiber (Q n) z) ≠ 0)
    (A : Set (S × V)) (hA : MeasurableSet A)
    (E : Set (S × V)) (hE : MeasurableSet[⨆ n, transverseLabelSigma (Q n)] E) :
    (∫ z in E,
      ((anchorNormalize (ρ.condKernel z.1) (⋂ n, labelFiber (Q n) z)).restrict
        (⋂ n, labelFiber (Q n) z)).real {t | (z.1,t) ∈ A} ∂ρ) = ρ.real (A ∩ E) := by
…

Mentions: OAI.DukePrimeDegree.transverseLabelSigma, OAI.DukePrimeDegree.labelFiber

theorem OAI.DukePrimeDegree.integral_countableFuture_conditional_probability line 92

Source documentation

The same preservation identity for the actual countable dynamical future, retaining any additional transverse coordinate.

theorem integral_countableFuture_conditional_probability
    {Y : Type*} [MeasurableSpace Y]
    (ρ : Measure (S × V)) [IsFiniteMeasure ρ]
    {Q : Y → ℕ} (hQ : Measurable Q) {T : Y → Y} (hT : Measurable T)
    {F : S × V → Y} (hF : Measurable F)
    (hpos : ∀ᵐ z ∂ρ, ρ.condKernel z.1 (countableFutureFiber T Q F z) ≠ 0)
    (A : Set (S × V)) (hA : MeasurableSet A) :
    let f := fun z =>
…

Mentions: OAI.DukePrimeDegree.countableFutureFiber

theorem OAI.DukePrimeDegree.setIntegral_countableFuture_conditional_probability line 111