RegularRootEntropyUpper.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Entropy upper bounds from small auxiliary root-orbit observations

The intrinsic stationary future kernel is built for the given bounded branching observation. An auxiliary observation only removes transverse coordinates from joint future fibers; it need not generate the ambient measurable space. Its sole entropy cost is its countable Shannon sum.

theorem OAI.DukePrimeDegree.heightClip_entropyRate_le_root_sum_add_auxiliary line 26

Source documentation

Each finite clip of a bounded branching observation is controlled by actual root information and the Shannon sum of the auxiliary observation. The stationary kernel and finite predecessor symbols are constructed in this proof, rather than supplied as additional hypotheses.

theorem heightClip_entropyRate_le_root_sum_add_auxiliary (d : ℕ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    (Q : X (d+1) → ℕ) (hQ : Measurable Q)
    (hbound : ∀ᵐ x ∂μ, ∀ v : UpperRootTime (d+1),
      (∀ k : ℕ,
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k]
          (rightAction x ((completeRootChain (d+1)).word v))) =
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] x)) →
      v ∈ (completeRootChain (d+1)).cube 1)
    (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
…

Mentions: OAI.DukePrimeDegree.UpperRootTime, OAI.DukePrimeDegree.completeRootChain

theorem OAI.DukePrimeDegree.negative_diagonal_entropy_le_root_sum_of_small_auxiliary line 127

Source documentation

Arbitrarily small auxiliary Shannon costs remove the transverse term. The bilateral neutral-fiber property belongs to Q itself; no generating property of the auxiliary observations is needed.

theorem negative_diagonal_entropy_le_root_sum_of_small_auxiliary (d : ℕ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    (Q : X (d+1) → ℕ) (hQ : Measurable Q)
    (hbound : ∀ᵐ x ∂μ, ∀ v : UpperRootTime (d+1),
      (∀ k : ℕ,
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k]
          (rightAction x ((completeRootChain (d+1)).word v))) =
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] x)) →
      v ∈ (completeRootChain (d+1)).cube 1)
    (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
…

Mentions: OAI.DukePrimeDegree.UpperRootTime, OAI.DukePrimeDegree.completeRootChain