RootPrefixNullStationarity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Future stationarity on measurable mass-containment events

A box restriction can be removed when the transverse leaf measure of the future outside that box vanishes. This event belongs to the future sigma algebra; no literal containment of the full fiber is required.

theorem OAI.DukePrimeDegree.RootPrefixBox.setIntegral_regularLeaf_wholeFuture_probability line 30

theorem OAI.DukePrimeDegree.RootPrefixBox.setIntegral_massContained_wholeFuture_probability line 83

Source documentation

Apply the local law directly on its canonical mass-containment event. Its measurability and the null-outside-box premise are proved.

theorem setIntegral_massContained_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)) μ]
    (hfree : ∀ᵐ x ∂μ, ∀ v ∈ positiveRootGeneratedGroup (allPositiveRoots (d+1)),
      rightAction x v = x → v = 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.positiveRootGeneratedGroup, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.completeRootChain, OAI.DukePrimeDegree.UpperRootTransverse