OAI/NumberTheory/DukePrimeDegree/Entropy/RegularEntropyScaling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.diagonal_regularEntropyTest_none line 15
2. theorem OAI.DukePrimeDegree.positive_entropy_regular_test line 28

   Source documentation

   The test weight indexed by none is the fourth iterate of the original regular diagonal transformation.

   theorem positive_entropy_regular_test (d : ℕ)
       (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
       (hA : ∀ u : LogCoordinates d,
         μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
       (hpos : 0 < measureEntropy μ (fun x => rightAction x
         (diagonalOneParameter (regularDiagonalWeights d) (regularDiagonalWeights_sum d) 1))) :
       0 < measureEntropy μ (fun x => rightAction x
         (diagonalOneParameter (regularEntropyTest d none) (regularEntropyTest_sum d none) 1)) := by
   …

   Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.regularEntropyTest, OAI.DukePrimeDegree.regularEntropyTest_sum