RootProductInformation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Information of products of the actual root leaf measures

Rectangular information of a finite product is the sum of its root information. Its integral is the coefficient-weighted sum of root information integrals.

def OAI.DukePrimeDegree.rootProductInformation line 27
Source documentation
Rectangular information in the product of the actual normalized root leaves, at independently prescribed real logarithmic scales.
```
def rootProductInformation (t : ι → ℝ) (x : X (d + 1)) : ℝ :=
…
```
lemma OAI.DukePrimeDegree.ae_rootProductInformation_eq_sum line 33
lemma OAI.DukePrimeDegree.integrable_rootProductInformation line 50
theorem OAI.DukePrimeDegree.integral_rootProductInformation line 60
Source documentation
The product leaf information has precisely the coefficient-weighted mean occurring in the entropy formula.
```
theorem integral_rootProductInformation (t : ι → ℝ) :
    (∫ x, rootProductInformation d i j hij μ t x ∂μ) =
      ∑ a, t a * canonicalRootCoefficient d μ (i a) (j a) := by
…
```
Mentions: OAI.DukePrimeDegree.rootProductInformation, OAI.DukePrimeDegree.canonicalRootCoefficient