RootHopf.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Hopf principle in an actual root box

A diagonal-invariant integrable observable is constant on almost every conditional root fiber whenever the diagonal direction has root weight one. The proof uses the actual root-box measure and its disintegration.

theorem OAI.DukePrimeDegree.ae_rootBox_eq_of_diagonal_invariant line 21

Source documentation

Stable root fibers carry constant values of invariant observables.

theorem ae_rootBox_eq_of_diagonal_invariant
    {n : ℕ} {i j k : Fin n} (hij : i ≠ j)
    (ell : Fin n → ℝ) (hell : ∑ r, ell r = 0) (hweight : ell i - ell j = 1)
    (μ : Measure (X n)) [IsFiniteMeasure μ] [μ.Regular]
    (B : RootBox hij k)
    (hT : MeasurePreserving (fun x => rightAction x (diagonalOneParameter ell hell 1)) μ μ)
    (f : X n → ℝ) (hf : Integrable f μ)
    (hfinv : (fun x => f (rightAction x (diagonalOneParameter ell hell 1))) =ᵐ[μ] f) :
    ∀ᵐ z ∂B.coordinateMeasure μ, ∀ᵐ t ∂B.conditionalKernel μ z.1,
      f (rootQuotientParametrization hij z) =
        f (rootQuotientParametrization hij (z.1, t)) := by
…