RegularRootEntropySandwich.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Regular entropy lower bounds and the upper-bound criterion

The expanding-root kernel gives one chamber's lower bound. Weyl covariance transports it to the opposite chamber. The finite regular upper estimates therefore imply the entropy identities and coefficient balance required by prime-degree rigidity.

lemma OAI.DukePrimeDegree.rootEntropyForm_neg_of_monotone line 22
lemma OAI.DukePrimeDegree.monotone_of_positive_root_gaps line 40
theorem OAI.DukePrimeDegree.rootEntropyForm_le_regular_entropy_neg line 56

theorem OAI.DukePrimeDegree.rootEntropyForm_le_regular_entropy_pos line 66

Source documentation

The forward-time lower bound uses numeric Weyl transport of the actual leaf coefficients, not an assumed coefficient symmetry.

theorem rootEntropyForm_le_regular_entropy_pos
    (ell : Fin (d + 1) → ℝ) (hell : ∑ i, ell i = 0)
    (hgap : ∀ p : allPositiveRoots (d + 1), Real.log 4 ≤ ell p.val.2 - ell p.val.1) :
    ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ) ell) ≤
      measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell 1)) := by
…

Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.rootEntropyForm, OAI.DukePrimeDegree.canonicalRootCoefficient

theorem OAI.DukePrimeDegree.regular_entropy_tests_lower line 103

Source documentation

Both signs of the finite regular tests have their unconditional root-information lower bound.

theorem regular_entropy_tests_lower (a : Option (Fin (d + 1))) :
    ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ) (regularEntropyTest d a)) ≤
        measureEntropy μ (fun x => rightAction x
          (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) 1)) ∧
    ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ)
      (fun i => -regularEntropyTest d a i)) ≤
        measureEntropy μ (fun x => rightAction x
          (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) (-1))) := by
…

Mentions: OAI.DukePrimeDegree.rootEntropyForm, OAI.DukePrimeDegree.canonicalRootCoefficient, OAI.DukePrimeDegree.regularEntropyTest, OAI.DukePrimeDegree.regularEntropyTest_sum

def OAI.DukePrimeDegree.CanonicalRegularEntropyUpperBounds line 120
Source documentation
The finite regular upper estimates, expressed without entropy identities.
```
def CanonicalRegularEntropyUpperBounds (d : ℕ) (μ : Measure (X (d + 1)))
    [IsProbabilityMeasure μ] : Prop :=
…
```
theorem OAI.DukePrimeDegree.canonicalRegularEntropyTests_of_upper_bounds line 131
theorem OAI.DukePrimeDegree.eklPrimeInput_of_regular_entropy_upper_bounds line 142
Source documentation
The finite regular upper estimates imply prime-degree entropy rigidity by the geometric rigidity theorem and both numerical lower bounds.
```
theorem eklPrimeInput_of_regular_entropy_upper_bounds (d : ℕ)
    (hupper : ∀ (μ : Measure (X (d + 1))) (hμ : IsProbabilityMeasure μ),
      ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ →
        @CanonicalRegularEntropyUpperBounds d μ hμ) :
    EKLPrimeInput d := by
…
```
Mentions: OAI.DukePrimeDegree.CanonicalRegularEntropyUpperBounds, OAI.DukePrimeDegree.EKLPrimeInput