OAI/NumberTheory/DukePrimeDegree/Entropy/RootInformationIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Signed mean information at every real time

Finite coefficients imply integrability. The actual leaf cocycle extends the mean identity to negative times as well as positive times.

  1. lemma OAI.DukePrimeDegree.integrable_rootInformation_nonneg line 25
  2. lemma OAI.DukePrimeDegree.integral_rootInformation_nonneg line 34
  3. lemma OAI.DukePrimeDegree.ae_rootInformation_time_reversal line 46
  4. theorem OAI.DukePrimeDegree.integrable_rootInformation line 59

    Source documentation

    Root information is integrable even for negative times.

    theorem integrable_rootInformation (t : ℝ) : Integrable (rootInformation hij μ t) μ := by
…
  5. theorem OAI.DukePrimeDegree.integral_rootInformation line 69

    Source documentation

    The signed integral is exactly linear at every real time.

    theorem integral_rootInformation (t : ℝ) :
    (∫ x, rootInformation hij μ t x ∂μ) = t * canonicalRootCoefficient d μ i j := by
…

    Mentions: OAI.DukePrimeDegree.canonicalRootCoefficient