AuxiliaryRootInformation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual root information bounds from auxiliary recurrent fibers

theorem OAI.DukePrimeDegree.RootPrefixCoordinates.predecessor_entropyRate_le_root_information_add_auxiliary line 18

Source documentation

Once the recurrent auxiliary observation removes the transverse coordinates, its only entropy cost is its countable Shannon sum. All kernel terms here are the intrinsic root-future measures.

theorem predecessor_entropyRate_le_root_information_add_auxiliary
    {d : ℕ} {P : Finset (Fin (d+1) × Fin (d+1))} {D : Finset (Fin (d+1))}
    {V : Type*} [TopologicalSpace V] [SecondCountableTopology V]
    [MeasurableSpace V] [BorelSpace V]
    (C : RootPrefixCoordinates (d+1) P V) (c : EliminationChain P D)
    (hP : InitialRootPattern P) (hf : c.finalEntries=allPositiveRoots (d+1))
    (z₀ : (UpperRootTransverse (d+1) × V) × c.Time)
    (μ : 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)
    (hbound : ∀ᵐ x ∂μ, ∃ R : ℝ, ∀ v : c.Time,
…

Mentions: OAI.DukePrimeDegree.RootPrefixCoordinates, OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.UpperRootTransverse