RemainingExpansionInformation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The mean normalization in the actual remaining-root covariance

lemma OAI.DukePrimeDegree.EliminationChain.remainingDilationCube_preimage line 18

theorem OAI.DukePrimeDegree.EliminationChain.ae_remainingExpansionMass_pos_ne_top line 35

Source documentation

Every expanding normalization rectangle has positive finite mass.

theorem ae_remainingExpansionMass_pos_ne_top (c : EliminationChain P D)
    (hP : InitialRootPattern P) (hf : c.finalEntries = allPositiveRoots (d+1))
    (ell : Fin (d+1) → ℝ) (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    ∀ᵐ x ∂μ,
      0 < c.remainingTimeProduct hP hf μ x ((c.rootDilation ell 1) ⁻¹' c.cube 1) ∧
      c.remainingTimeProduct hP hf μ x ((c.rootDilation ell 1) ⁻¹' c.cube 1) ≠ ∞ := by
…

Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.EliminationChain.remainingExpansionInformation_integrable_integral line 63
Source documentation
Logarithm of the covariance normalizing mass. It is integrable, and its mean is the signed root-character sum, for arbitrary weights.
```
theorem remainingExpansionInformation_integrable_integral (c : EliminationChain P D)
    (hP : InitialRootPattern P) (hf : c.finalEntries = allPositiveRoots (d+1))
    (ell : Fin (d+1) → ℝ) (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    let J := fun x => Real.log
…
```
Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.InitialRootPattern, OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.diagonalFlow