CanonicalRootBasic.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Mean root coefficients and their elementary properties

The coefficient is the mean leaf information at unit scale. Diagonal covariance makes real-time mean information linear in time.

def OAI.DukePrimeDegree.canonicalRootCoefficient line 20
Source documentation
The actual mean information at unit scale, with zero diagonal.
```
def canonicalRootCoefficient (d : ℕ) (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (i j : Fin (d + 1)) : ℝ :=
…
```
lemma OAI.DukePrimeDegree.canonicalRootCoefficient_diagonal line 27
lemma OAI.DukePrimeDegree.canonicalRootCoefficient_nonneg line 30
lemma OAI.DukePrimeDegree.canonicalRootCoefficient_le_one line 39
lemma OAI.DukePrimeDegree.canonicalRootCoefficient_zero_iff line 47
lemma OAI.DukePrimeDegree.canonicalRootCoefficient_one_of_invariant line 56

lemma OAI.DukePrimeDegree.rootInformationMean_eq_coefficient line 64

Source documentation

Actual real-time mean information is the root coefficient times time.

lemma rootInformationMean_eq_coefficient (i j : Fin (d + 1)) (hij : i ≠ j)
    {t : ℝ} (ht : 0 ≤ t) :
    rootInformationMean hij μ t =
      ENNReal.ofReal (t * canonicalRootCoefficient d μ i j) := by
…

Mentions: OAI.DukePrimeDegree.canonicalRootCoefficient