LeafMaximalDisintegration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Disintegrating the relative leaf maximal estimate

The real-line estimate is integrated against the transverse measure. This gives the relative maximal bound in an actual root box, using its conditional kernel and the original ambient measure.

theorem OAI.DukePrimeDegree.relative_maximal_compProd_bound line 20

theorem OAI.DukePrimeDegree.exists_rootBox_relative_maximal_constant line 41

Source documentation

The Besicovitch constant remains uniform after integrating along the actual conditional distributions in any root box.

theorem exists_rootBox_relative_maximal_constant :
    ∃ N : ℕ, ∀ {n : ℕ} {i j k : Fin n} (hij : i ≠ j)
      (A : RootBox hij k) (μ : Measure (X n)) [IsFiniteMeasure μ]
      (B E : Set (X n)), MeasurableSet B → MeasurableSet E → ∀ c : ℝ≥0∞,
      (∀ᵐ s ∂(A.coordinateMeasure μ).fst, ∀ᵐ t ∂A.conditionalKernel μ s,
        rootQuotientParametrization hij (s, t) ∈ B → ∃ r : ℝ, 0 < r ∧
        c * A.conditionalKernel μ s (closedBall t r) ≤
          A.conditionalKernel μ s
            ({u | rootQuotientParametrization hij (s, u) ∈ E} ∩ closedBall t r)) →
      c * (μ.restrict A.range) B ≤ (N : ℝ≥0∞) * (μ.restrict A.range) E := by
…