OAI/NumberTheory/DukePrimeDegree/Geometry/RootTranslateLeaves.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Translation covariance of the global normalized root leaf

Long root boxes extend the local disintegration identity to the whole real root line. Centering cancels the translation, so a preserving root translation fixes the intrinsic normalized leaf almost everywhere.

  1. theorem OAI.DukePrimeDegree.RootBox.ae_leafMeasure_translate line 24
  2. lemma OAI.DukePrimeDegree.RootBox.translate_time_bound line 92
  3. lemma OAI.DukePrimeDegree.RootBox.ae_basedLeaf_translate line 101
  4. lemma OAI.DukePrimeDegree.RootBox.ae_intrinsicRootLeaf_translate_restrict line 116
  5. theorem OAI.DukePrimeDegree.ae_intrinsicRootLeaf_translate line 138

    Source documentation

    A preserving root translation fixes the normalized intrinsic leaf.

    theorem ae_intrinsicRootLeaf_translate {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (a : ℝ) (μ : Measure (X n)) [IsFiniteMeasure μ]
    (hfree : ∀ᵐ x ∂μ, ∀ v : ℝ,
      rightAction x (Matrix.SpecialLinearGroup.transvection hij v) = x → v = 0)
    (hinv : μ.map (fun x => rightAction x (Matrix.SpecialLinearGroup.transvection hij a)) = μ) :
    ∀ᵐ x ∂μ, intrinsicRootLeaf hij μ
      (rightAction x (Matrix.SpecialLinearGroup.transvection hij a)) = intrinsicRootLeaf hij μ x := by
…