RootPrefixFutureStationarity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Local stationarity of the actual whole-future root conditional

The normalized root-product description inherits the disintegration identity on each genuine box. If that box contains the entire future fiber, its arbitrary box normalization can be removed.

lemma OAI.DukePrimeDegree.normalized_restriction_nested line 20

theorem OAI.DukePrimeDegree.RootPrefixBox.integral_intrinsicProduct_future_probability line 39

Source documentation

Every measurable coordinate event has its original mass after integration against the actual intrinsic-product future conditionals.

theorem integral_intrinsicProduct_future_probability
    (B : RootPrefixBox C c hP₀ hf g) (R : ℝ) (hBR : B.time ⊆ c.remainingWindow R 0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    {Q : X (d+1) → ℕ} (hQ : Measurable Q)
    {T : X (d+1) → X (d+1)} (hT : Measurable T)
    (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
      Q (T^[k] (rightAction x ((completeRootChain (d+1)).word v)))=Q (T^[k] x))
    (A : Set ((UpperRootTransverse (d+1) × V) × c.Time)) (hA : MeasurableSet A) :
    let F := C.timeParam c hP₀ hf g
…

Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.completeRootChain, OAI.DukePrimeDegree.UpperRootTransverse

theorem OAI.DukePrimeDegree.RootPrefixBox.integral_uncentered_wholeFuture_probability line 75

Source documentation

For a box containing the entire future fiber, local stationarity uses the unnormalized intrinsic product directly.

theorem integral_uncentered_wholeFuture_probability
    (B : RootPrefixBox C c hP₀ hf g) (R : ℝ) (hBR : B.time ⊆ c.remainingWindow R 0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    {Q : X (d+1) → ℕ} (hQ : Measurable Q)
    {T : X (d+1) → X (d+1)} (hT : Measurable T)
    (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
      Q (T^[k] (rightAction x ((completeRootChain (d+1)).word v)))=Q (T^[k] x))
    (hcontained : ∀ᵐ z ∂B.coordinateMeasure μ,
      countableFutureFiber T Q (C.timeParam c hP₀ hf g) z ⊆ B.time)
    (A : Set ((UpperRootTransverse (d+1) × V) × c.Time)) (hA : MeasurableSet A) :
    let F := C.timeParam c hP₀ hf g
…

Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.completeRootChain, OAI.DukePrimeDegree.countableFutureFiber, OAI.DukePrimeDegree.UpperRootTransverse

theorem OAI.DukePrimeDegree.RootPrefixBox.setIntegral_uncentered_wholeFuture_probability line 116

Source documentation

Restriction to a future event commutes with local disintegration. The whole future need be inside the box only on that event.

theorem setIntegral_uncentered_wholeFuture_probability
    (B : RootPrefixBox C c hP₀ hf g) (R : ℝ) (hBR : B.time ⊆ c.remainingWindow R 0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    {Q : X (d+1) → ℕ} (hQ : Measurable Q)
    {T : X (d+1) → X (d+1)} (hT : Measurable T)
    (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
      Q (T^[k] (rightAction x ((completeRootChain (d+1)).word v)))=Q (T^[k] x))
    (E : Set ((UpperRootTransverse (d+1) × V) × c.Time))
    (hE : MeasurableSet[⨆ m, transverseLabelSigma
      (fun z => countableFutureCode T Q m (C.timeParam c hP₀ hf g z))] E)
    (hcontained : ∀ᵐ z ∂(B.coordinateMeasure μ).restrict E,
…

Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.completeRootChain, OAI.DukePrimeDegree.UpperRootTransverse, OAI.DukePrimeDegree.transverseLabelSigma, OAI.DukePrimeDegree.countableFutureCode