RegularEntropyDischarge.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The finite regular entropy identities and prime-degree rigidity

The negative-time upper bound uses the actual root-future construction. Weyl reindexing supplies the positive-time upper bound with the actual transported leaf coefficients. Together with the proved lower bounds, these discharge the finite regular tests and the prime-degree EKL input.

theorem OAI.DukePrimeDegree.regular_entropy_le_root_form_neg line 25

Source documentation

The actual negative-time entropy is bounded by its canonical root form.

theorem regular_entropy_le_root_form_neg
    (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) :
    measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell (-1))) ≤
      ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ) (fun i => -ell i)) := by
…

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

theorem OAI.DukePrimeDegree.regular_entropy_le_root_form_pos line 42

Source documentation

Reverse the coordinate order and weights to obtain the positive-time bound without assuming symmetry of opposite root coefficients.

theorem regular_entropy_le_root_form_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) :
    measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell 1)) ≤
      ENNReal.ofReal (rootEntropyForm (canonicalRootCoefficient d μ) ell) := by
…

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

theorem OAI.DukePrimeDegree.canonicalRegularEntropyUpperBounds_proved line 78
Source documentation
Both finite families of regular upper bounds hold without additional entropy or leaf-measure hypotheses.
```
theorem canonicalRegularEntropyUpperBounds_proved : CanonicalRegularEntropyUpperBounds d μ := by
…
```
Mentions: OAI.DukePrimeDegree.CanonicalRegularEntropyUpperBounds
theorem OAI.DukePrimeDegree.canonicalRegularEntropyTests_proved line 87
Source documentation
Exact regular entropy identities, using the intrinsic coefficients.
```
theorem canonicalRegularEntropyTests_proved : CanonicalRegularEntropyTests d μ :=
…
```
Mentions: OAI.DukePrimeDegree.CanonicalRegularEntropyTests
theorem OAI.DukePrimeDegree.rootInvarianceRelation_symmetric_proved line 91
Source documentation
The actual invariant-root relation is symmetric.
```
theorem rootInvarianceRelation_symmetric_proved (hd : 2 < d+1) :
    Std.Symm (rootInvarianceRelation μ) :=
…
```

theorem OAI.DukePrimeDegree.isHaar_of_prime_positive_regular_entropy line 96

Source documentation

Positive regular entropy forces Haar probability in prime degree.

theorem isHaar_of_prime_positive_regular_entropy (hprime : (d+1).Prime) (hd : 2 < d+1)
    (hpos : 0 < measureEntropy μ (fun x => rightAction x
      (diagonalOneParameter (regularDiagonalWeights d) (regularDiagonalWeights_sum d) 1))) :
    IsHaarProbability μ :=
…

theorem OAI.DukePrimeDegree.eklPrimeInput_unconditional line 106
Source documentation
The published rigidity specialization required by the packet proof, with all its mathematical input proved for this application.
```
theorem eklPrimeInput_unconditional (d : ℕ) : EKLPrimeInput d := by
…
```
Mentions: OAI.DukePrimeDegree.EKLPrimeInput