RegularEntropyTests.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finitely many regular weights suffice for coefficient balance

For the prime-degree application the balance argument does not need the entropy formula at singular weights. One regular weight and one small perturbation for each coordinate suffice, together with their negatives. All positive gaps in these explicit weights are at least log 4.

def OAI.DukePrimeDegree.rawEntropyTest line 20
def OAI.DukePrimeDegree.regularEntropyTest line 23
lemma OAI.DukePrimeDegree.regularEntropyTest_none line 26
lemma OAI.DukePrimeDegree.regularEntropyTest_sum line 32
lemma OAI.DukePrimeDegree.regularEntropyTest_gap line 41
lemma OAI.DukePrimeDegree.rootEntropyForm_skew line 54
lemma OAI.DukePrimeDegree.rootEntropyForm_skew_add line 73
lemma OAI.DukePrimeDegree.regularEntropyTest_skew line 85
theorem OAI.DukePrimeDegree.balanced_of_regularEntropyTest_symmetry line 101
Source documentation
Balance needs only the explicit finite regular test family and its negatives, not the formula on arbitrary or singular diagonal weights.
```
theorem balanced_of_regularEntropyTest_symmetry {d : ℕ}
    (w : Fin (d+1) → Fin (d+1) → ℝ)
    (hsym : ∀ a : Option (Fin (d+1)),
      rootEntropyForm w (regularEntropyTest d a) =
        rootEntropyForm w (fun i => -regularEntropyTest d a i)) :
    ∀ i, ∑ j, w i j = ∑ j, w j i := by
…
```
Mentions: OAI.DukePrimeDegree.rootEntropyForm, OAI.DukePrimeDegree.regularEntropyTest

theorem OAI.DukePrimeDegree.balanced_of_regular_diagonal_entropy_tests line 128

Source documentation

The finite test formulas are the only entropy identities needed by coefficient balance, together with invariance of entropy under time reversal.

theorem balanced_of_regular_diagonal_entropy_tests
    (d : ℕ) (μ : MeasureTheory.Measure (PrimeDegreePackets.X (d+1)))
    (hA : ∀ u : PrimeDegreePackets.LogCoordinates d,
      μ.map (fun x => PrimeDegreePackets.rightAction x (PrimeDegreePackets.diagonalFlow u))=μ)
    (w : Fin (d+1) → Fin (d+1) → ℝ) (hw : ∀ i j, 0 ≤ w i j)
    (htests : ∀ a : Option (Fin (d+1)),
      PrimeDegreePackets.measureEntropy μ (fun x => PrimeDegreePackets.rightAction x
        (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) 1)) =
          ENNReal.ofReal (rootEntropyForm w (regularEntropyTest d a)) ∧
      PrimeDegreePackets.measureEntropy μ (fun x => PrimeDegreePackets.rightAction x
        (diagonalOneParameter (regularEntropyTest d a) (regularEntropyTest_sum d a) (-1))) =
          ENNReal.ofReal (rootEntropyForm w (fun i => -regularEntropyTest d a i))) :
…

Mentions: OAI.PrimeDegreePackets.X, OAI.PrimeDegreePackets.LogCoordinates, OAI.PrimeDegreePackets.rightAction, OAI.PrimeDegreePackets.diagonalFlow, OAI.PrimeDegreePackets.measureEntropy, OAI.DukePrimeDegree.regularEntropyTest, OAI.DukePrimeDegree.regularEntropyTest_sum, OAI.DukePrimeDegree.rootEntropyForm