LeafSmallRadius.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform small-radius control of nonatomic root leaves

The set denoted X_ρ in EKL (2006), Section 4.3, can have arbitrarily large measure. The proof uses continuity from above twice: first on each locally finite leaf, and then on the decreasing sets of bad base points.

lemma OAI.DukePrimeDegree.exists_small_ball_mass_of_zero_atom line 20

theorem OAI.DukePrimeDegree.exists_uniform_small_kernel_ball line 38

Source documentation

One radius works outside an arbitrarily small set of base points.

theorem exists_uniform_small_kernel_ball
    {Y : Type*} [MeasurableSpace Y] (μ : Measure Y) [IsFiniteMeasure μ]
    (κ : Kernel Y ℝ)
    (hfinite : ∀ᵐ x ∂μ, κ x (Metric.ball 0 1) ≠ ∞)
    (hzero : ∀ᵐ x ∂μ, κ x {0} = 0)
    (c ε : ℝ≥0∞) (hc : 0 < c) (hε : ε ≠ 0) :
    ∃ ρ : ℝ, 0 < ρ ∧ ρ < 1 / 2 ∧
      μ {x | c ≤ κ x (Metric.ball 0 ρ)} < ε := by
…

theorem OAI.DukePrimeDegree.exists_uniform_small_rootLeaf_ball line 84

Source documentation

The uniform-radius set for the actual intrinsic root leaves.

theorem exists_uniform_small_rootLeaf_ball
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (hnontrivial : ∀ᵐ x ∂μ, intrinsicRootLeaf hij μ x ≠ Measure.dirac 0)
    (c ε : ℝ≥0∞) (hc : 0 < c) (hε : ε ≠ 0) :
    ∃ ρ : ℝ, 0 < ρ ∧ ρ < 1 / 2 ∧
      μ {x | c ≤ intrinsicRootLeaf hij μ x (Metric.ball 0 ρ)} < ε := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow