Measure domination from eventual small-ball estimates

Definition

KLSModular_FunctionalInequalities_Probability_Domination_Ball

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

FunctionalInequalities.Probability.measure_le_smul_of_eventually_closedBall_le states that, in a finite-dimensional real normed Borel space, if locally finite measures μ and m satisfy $\mu(\overline B(x,r))\le C\,m(\overline B(x,r))$ for all sufficiently small positive radii at every center, then $\mu\le C\,m$ as measures, with $C$ a nonnegative real constant. absolutelyContinuous_of_eventually_closedBall_le gives the corresponding absolute continuity conclusion $\mu\ll m$ . The radius threshold may depend on the center, while the multiplier C is uniform.

Original module imports

import Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Original declaration excerpt

Shown in the original module context. Body omitted.

theorem measure_le_smul_of_eventually_closedBall_le (μ m : Measure E)
    [IsLocallyFiniteMeasure μ] [IsLocallyFiniteMeasure m] (C : NNReal)
    (h : ∀ x : E, ∀ᶠ r : ℝ in 𝓝[>] 0,
      μ (closedBall x r) ≤ (C : ENNReal) * m (closedBall x r)) :
    μ ≤ (C : ENNReal) • m

Module navigation

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.Domination.Ball · Frozen source 408915f.

Definition code

import Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

noncomputable section
open MeasureTheory Filter Metric Topology
namespace FunctionalInequalities
namespace Probability
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
/-- A uniform finite bound on sufficiently small ball ratios implies domination on every
measurable set. The admissible radius may depend on the center. -/
theorem measure_le_smul_of_eventually_closedBall_le (μ m : Measure E)
    [IsLocallyFiniteMeasure μ] [IsLocallyFiniteMeasure m] (C : NNReal)
    (h : ∀ x : E, ∀ᶠ r : ℝ in 𝓝[>] 0,
      μ (closedBall x r) ≤ (C : ENNReal) * m (closedBall x r)) :
    μ ≤ (C : ENNReal) • m := by
  have : IsLocallyFiniteMeasure ((C : ENNReal) • m) := by
    change IsLocallyFiniteMeasure (C • m)
    infer_instance
  apply Measure.le_iff.mpr
  intro s _
  apply (Besicovitch.vitaliFamily μ).measure_le_of_frequently_le
    ((C : ENNReal) • m) Measure.AbsolutelyContinuous.rfl s
  intro x _
  apply (Besicovitch.tendsto_filterAt μ x).frequently
  exact (h x).mono (by intro r hr; simpa using hr) |>.frequently
/-- Small-ball domination supplies absolute continuity without assuming it in the covering
step. The Vitali family is built for the source measure itself. -/
theorem absolutelyContinuous_of_eventually_closedBall_le (μ m : Measure E)
    [IsLocallyFiniteMeasure μ] [IsLocallyFiniteMeasure m] (C : NNReal)
    (h : ∀ x : E, ∀ᶠ r : ℝ in 𝓝[>] 0,
      μ (closedBall x r) ≤ (C : ENNReal) * m (closedBall x r)) : μ ≪ m :=
  Measure.absolutelyContinuous_of_le_smul (measure_le_smul_of_eventually_closedBall_le μ m C h)
end Probability
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Domination/Ball.lean#L20-L44 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Domination.Ball`, definition bundle `KLSModular_FunctionalInequalities_Probability_Domination_Ball`; the repository is private at upload time).

View graph