OAI/NumberTheory/DukePrimeDegree/Dynamics/RootInvariantLeaves.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Lebesgue normalization for invariant roots

A preserving root action fixes its intrinsic leaf. The pointwise rebasing law turns this into projective translation periods; diagonal covariance removes their multipliers. Arbitrarily small periods identify Lebesgue measure, giving the exact mean information coefficient one.

  1. lemma OAI.DukePrimeDegree.ae_based_fixed_of_root_invariant line 27
  2. theorem OAI.DukePrimeDegree.ae_rootLeaf_invariant_of_root_invariant line 47

    Source documentation

    Every invariant root has translation-invariant intrinsic conditionals.

    theorem ae_rootLeaf_invariant_of_root_invariant
    (hinv : ∀ a : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij a)) = μ) :
    ∀ᵐ x ∂μ, ∀ a : ℝ,
      (intrinsicRootLeaf hij μ x).map (fun t => t + a) = intrinsicRootLeaf hij μ x := by
…
  3. theorem OAI.DukePrimeDegree.ae_rootLeaf_eq_half_volume line 75

    Source documentation

    Unit mass on the unit ball fixes the Haar scalar to one half.

    theorem ae_rootLeaf_eq_half_volume
    (hinv : ∀ a : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij a)) = μ) :
    ∀ᵐ x ∂μ, intrinsicRootLeaf hij μ x = (2 : ℝ≥0∞)⁻¹ • (volume : Measure ℝ) := by
…
  4. theorem OAI.DukePrimeDegree.ae_rootInformation_of_invariant line 91
  5. theorem OAI.DukePrimeDegree.rootInformationMean_of_invariant line 108

    Source documentation

    Haar root conditionals give coefficient one in the actual leaf information.

    theorem rootInformationMean_of_invariant [IsProbabilityMeasure μ]
    (hinv : ∀ a : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij a)) = μ) (t : ℝ) :
    rootInformationMean hij μ t = ENNReal.ofReal t := by
…