DensityTruncation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Truncation of radial densities

The integer-cap step prep:integer-caps deletes pairs on which either radial density exceeds a threshold. These lemmas estimate the deleted original product mass by the Lp moments and bound every remaining fiber by the threshold times the angular reference measure.

theorem OAI.Falconer.ennreal_le_threshold_tail line 20

theorem OAI.Falconer.density_tail_mass line 41

Source documentation

The density mass above T is bounded by T^(1-p) times its pth moment.

theorem density_tail_mass {A : Type*} [MeasurableSpace A]
    (σ : Measure A) (f : A → ℝ≥0∞) (hf : Measurable f)
    {T : ℝ≥0∞} {p : ℝ} (hT : 0 < T) (hTtop : T ≠ ∞) (hp : 1 < p) :
    (σ.withDensity f) {a | T < f a} ≤ T ^ (1 - p) * ∫⁻ a, f a ^ p ∂σ := by
…

theorem OAI.Falconer.truncated_density_mass line 59

Source documentation

Truncation leaves a density bounded by the threshold on every cap.

theorem truncated_density_mass {A : Type*} [MeasurableSpace A]
    (σ : Measure A) (f : A → ℝ≥0∞) (hf : Measurable f)
    (T : ℝ≥0∞) (S : Set A) (hS : MeasurableSet S) :
    (σ.withDensity f) (S ∩ {a | f a ≤ T}) ≤ T * σ S := by
…

def OAI.Falconer.densityFailure line 75

Source documentation

The bad pairs for one orientation of a radial kernel.

def densityFailure {X Y A : Type*} (f : X × A → ℝ≥0∞)
    (r : X × Y → A) (T : ℝ≥0∞) : Set (X × Y) :=
…

theorem OAI.Falconer.measurableSet_densityFailure line 79

theorem OAI.Falconer.density_failure_product_mass line 87

Source documentation

Fubini measures failure using the original source marginal and the original pin marginal. There is no normalization of individual fibers.

theorem density_failure_product_mass {X Y A : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace A]
    (μ : Measure X) (ν : Measure Y) [SFinite ν] (σ : Measure A)
    (f : X × A → ℝ≥0∞) (r : X × Y → A) (hf : Measurable f) (hr : Measurable r)
    (hdensity : ∀ᵐ x ∂μ, ν.map (fun y => r (x, y)) = σ.withDensity (fun a => f (x, a)))
    {T : ℝ≥0∞} {p : ℝ} (hT : 0 < T) (hTtop : T ≠ ∞) (hp : 1 < p) :
    (μ.prod ν) (densityFailure f r T) ≤
      T ^ (1 - p) * ∫⁻ x, ∫⁻ a, f (x, a) ^ p ∂σ ∂μ := by
…

Mentions: OAI.Falconer.densityFailure

theorem OAI.Falconer.truncated_radial_fiber line 109

Source documentation

Any additional pair restriction preserves the truncated fiber bound.

theorem truncated_radial_fiber {Y A : Type*} [MeasurableSpace Y] [MeasurableSpace A]
    (ν : Measure Y) (σ : Measure A) (f : A → ℝ≥0∞) (r : Y → A)
    (hf : Measurable f) (hr : Measurable r) (hdensity : ν.map r = σ.withDensity f)
    (T : ℝ≥0∞) (H : Set Y) (hH : ∀ y ∈ H, f (r y) ≤ T)
    (S : Set A) (hS : MeasurableSet S) :
    ν (H ∩ r ⁻¹' S) ≤ T * σ S := by
…

theorem OAI.Falconer.bilateral_density_failure_mass line 126

Source documentation

Deleting the failures in both orientations costs the sum of the two integrated radial pth moments.

theorem bilateral_density_failure_mass {X Y A : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace A]
    (μ : Measure X) (ν : Measure Y) [SFinite μ] [SFinite ν] (σ : Measure A)
    (f : X × A → ℝ≥0∞) (r : X × Y → A) (g : Y × A → ℝ≥0∞) (s : Y × X → A)
    (hf : Measurable f) (hr : Measurable r) (hg : Measurable g) (hs : Measurable s)
    (hfdensity : ∀ᵐ x ∂μ, ν.map (fun y => r (x, y)) = σ.withDensity (fun a => f (x, a)))
    (hgdensity : ∀ᵐ y ∂ν, μ.map (fun x => s (y, x)) = σ.withDensity (fun a => g (y, a)))
    {T : ℝ≥0∞} {p : ℝ} (hT : 0 < T) (hTtop : T ≠ ∞) (hp : 1 < p) :
    (μ.prod ν) (densityFailure f r T ∪ Prod.swap ⁻¹' densityFailure g s T) ≤
      T ^ (1 - p) * ((∫⁻ x, ∫⁻ a, f (x, a) ^ p ∂σ ∂μ) +
        ∫⁻ y, ∫⁻ a, g (y, a) ^ p ∂σ ∂ν) := by
…

Mentions: OAI.Falconer.densityFailure

theorem OAI.Falconer.exists_density_tail_power_bound line 152

Source documentation

The threshold R^(e/2) gives a positive power saving in deleted mass for every p > 1; its exponent is exactly e * (p - 1) / 2.

theorem exists_density_tail_power_bound (M : ℝ≥0∞) (hM : M ≠ ∞)
    {e p : ℝ} (he : 0 < e) (hp : 1 < p) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ R : ℝ, 0 < R →
      (ENNReal.ofReal (R ^ (e / 2))) ^ (1 - p) * M ≤
        ENNReal.ofReal (C * R ^ (-c)) := by
…

theorem OAI.Falconer.measurable_radialDirection_joint line 173