OAI/NumberTheory/DukePrimeDegree/Entropy/RootInformationScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact scaling of the mean root information

The actual normalized leaf information is additive under the canonical flow. Monotonicity and rational approximation promote its integer-time scaling law to every nonnegative real time, including infinite means.

  1. def OAI.DukePrimeDegree.rootInformationHom line 26
  2. lemma OAI.DukePrimeDegree.rootInformationMean_mono line 31
  3. lemma OAI.DukePrimeDegree.rootInformationMean_rat line 38
  4. theorem OAI.DukePrimeDegree.rootInformationMean_real line 61

    Source documentation

    The mean at time one is the exact coefficient at every positive scale.

    theorem rootInformationMean_real {t : ℝ} (ht : 0 ≤ t) :
    rootInformationMean hij μ t =
      ENNReal.ofReal t * rootInformationMean hij μ 1 := by
…