RemainingFutureInformation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Mean information of the actual whole-future root atom

theorem OAI.DukePrimeDegree.EliminationChain.remainingFutureInformation_integrable_integral line 20

Source documentation

Positive finite whole-future mass converts exact leaf covariance into an integrable information function with the canonical root mean.

theorem remainingFutureInformation_integrable_integral (d : ℕ)
    {P : Finset (Fin (d+1) × Fin (d+1))} {D : Finset (Fin (d+1))}
    (c : EliminationChain P D) (hP : InitialRootPattern P)
    (hf : c.finalEntries = allPositiveRoots (d+1))
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k = 0)
    (Q : X (d+1) → ℕ) (hQ : Measurable Q)
    (hmass : ∀ᵐ x ∂μ,
      0 < c.remainingTimeProduct hP hf μ x (c.remainingFutureAtom ell hell Q 0 x) ∧
      c.remainingTimeProduct hP hf μ x (c.remainingFutureAtom ell hell Q 0 x) ≤ 1) :
    let I := fun x => -Real.log
…

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