RootLeafHopf.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Neutral root leaves are constant along contracting root fibers

Bounded transforms let the scalar Hopf theorem apply to every measurable leaf-test integral. The countable determining family for locally finite real measures then gives equality of the leaf kernels themselves.

theorem OAI.DukePrimeDegree.ae_rootBox_eq_of_measurable_diagonal_invariant line 21

theorem OAI.DukePrimeDegree.ae_intrinsicRootKernel_neutral line 47

Source documentation

A neutral diagonal direction preserves a root kernel almost everywhere.

theorem ae_intrinsicRootKernel_neutral
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ r, ell r = 0) (hneutral : ell i = ell j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (hfree : ∀ᵐ x ∂μ, ∀ v : ℝ,
      rightAction x (Matrix.SpecialLinearGroup.transvection hij v) = x → v = 0)
    (t : ℝ) :
    ∀ᵐ x ∂μ, intrinsicRootKernel hij μ hfree
      (rightAction x (diagonalOneParameter ell hell t)) = intrinsicRootKernel hij μ hfree x := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.ae_rootBox_intrinsicKernel_eq line 71

Source documentation

Countably many leaf tests identify the kernel on a contracting root fiber.

theorem ae_rootBox_intrinsicKernel_eq
    (d : ℕ) {i j k l p : Fin (d + 1)} (hij : i ≠ j) (hkl : k ≠ l)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ r, ell r = 0)
    (hneutral : ell i = ell j) (hweight : ell k - ell l = 1)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ] [μ.Regular]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (hfree : ∀ᵐ x ∂μ, ∀ v : ℝ,
      rightAction x (Matrix.SpecialLinearGroup.transvection hij v) = x → v = 0)
    (B : RootBox hkl p) :
    ∀ᵐ z ∂B.coordinateMeasure μ, ∀ᵐ t ∂B.conditionalKernel μ z.1,
      intrinsicRootKernel hij μ hfree (rootQuotientParametrization hkl z) =
        intrinsicRootKernel hij μ hfree (rootQuotientParametrization hkl (z.1, t)) := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.ae_rootBox_intrinsicLeaf_eq line 107

Source documentation

The intrinsic leaf itself is unchanged on those same conditional fibers.

theorem ae_rootBox_intrinsicLeaf_eq
    (d : ℕ) {i j k l p : Fin (d + 1)} (hij : i ≠ j) (hkl : k ≠ l)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ r, ell r = 0)
    (hneutral : ell i = ell j) (hweight : ell k - ell l = 1)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ] [μ.Regular]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (B : RootBox hkl p) :
    ∀ᵐ z ∂B.coordinateMeasure μ, ∀ᵐ t ∂B.conditionalKernel μ z.1,
      intrinsicRootLeaf hij μ (rootQuotientParametrization hkl z) =
        intrinsicRootLeaf hij μ (rootQuotientParametrization hkl (z.1, t)) := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

theorem OAI.DukePrimeDegree.ae_rootBox_intrinsicLeaf_eq_of_nonparallel line 141

Source documentation

Any nonparallel root admits a neutral contracting direction, so the intrinsic leaf is constant on its conditional fibers.

theorem ae_rootBox_intrinsicLeaf_eq_of_nonparallel
    (d : ℕ) {i j k l p : Fin (d + 1)} (hij : i ≠ j) (hkl : k ≠ l)
    (hforward : ¬ (k = i ∧ l = j)) (hbackward : ¬ (k = j ∧ l = i))
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ] [μ.Regular]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (B : RootBox hkl p) :
    ∀ᵐ z ∂B.coordinateMeasure μ, ∀ᵐ t ∂B.conditionalKernel μ z.1,
      intrinsicRootLeaf hij μ (rootQuotientParametrization hkl z) =
        intrinsicRootLeaf hij μ (rootQuotientParametrization hkl (z.1, t)) := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow