RootPrefixFutureIntegral.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the exact whole-future information in a root box

The result retains the restriction to the actual box range. It is not a replacement of that restricted integral by the global canonical mean.

theorem OAI.DukePrimeDegree.RootPrefixBox.wholeFuture_conditionalInformation_integrable_integral line 29

Source documentation

Integrability and the exact ambient restricted integral follow from positive finite future mass and the local conditional probability formula.

theorem wholeFuture_conditionalInformation_integrable_integral
    (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)) μ]
    (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k=0) (Q : X (d+1) → ℕ)
    (hQ : Measurable Q)
    (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
      Q ((fun x => rightAction x (diagonalOneParameter ell hell (-1)))^[k]
        (rightAction x ((completeRootChain (d+1)).word v))) =
      Q ((fun x => rightAction x (diagonalOneParameter ell hell (-1)))^[k] x))
    (hmass : ∀ᵐ x ∂μ,
      0 < c.remainingTimeProduct hP₀ hf μ x (c.remainingFutureAtom ell hell Q 0 x) ∧
…

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