VolumeBudget.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The dyadic volume-defect budget

Successive volume increments telescope, while the rescaled curvature contribution is a geometric series. Both monotone bounded profiles and raw profiles converging to a bounded density are treated. This is the scalar summation argument in the proof of the manuscript's Poisson pinching lemma.

theorem OAI.RegularPointCoordinates.volume_profile_increment_sum line 23
Source documentation
The finite sum of consecutive normalized-volume increments telescopes.
```
theorem volume_profile_increment_sum (A : ℕ → ℝ) (k : ℕ) :
    (∑ i ∈ Finset.range k, (A (i + 1) - A i)) = A k - A 0 := by
…
```
theorem OAI.RegularPointCoordinates.sum_range_quarter_pow_le line 32
Source documentation
The curvature correction at dyadic radii has total mass at most 4 / 3.
```
theorem sum_range_quarter_pow_le (k : ℕ) :
    (∑ i ∈ Finset.range k, (1 / 4 : ℝ) ^ i) ≤ 4 / 3 := by
…
```
theorem OAI.RegularPointCoordinates.volume_profile_increments_summable line 48
Source documentation
A monotone volume profile bounded by Euclidean volume has summable successive increments.
```
theorem volume_profile_increments_summable {A : ℕ → ℝ} {omega : ℝ}
    (hmono : Monotone A) (hupper : ∀ i, A i ≤ omega) :
    Summable (fun i => A (i + 1) - A i) := by
…
```

theorem OAI.RegularPointCoordinates.volume_defect_partial_sum_telescope line 59

Source documentation

Finite Poisson-defect sums are controlled by the corresponding volume drop and the partial curvature series.

theorem volume_defect_partial_sum_telescope {A P : ℕ → ℝ} {C kappa : ℝ}
    (hbound : ∀ i, P i ≤ C * (A (i + 1) - A i + kappa * (1 / 4 : ℝ) ^ i))
    (k : ℕ) :
    (∑ i ∈ Finset.range k, P i) ≤
      C * (A k - A 0 + kappa * ∑ i ∈ Finset.range k, (1 / 4 : ℝ) ^ i) := by
…

theorem OAI.RegularPointCoordinates.volume_defect_partial_sum_le line 71

Source documentation

Uniform finite-scale bound by the initial volume deficit and curvature.

theorem volume_defect_partial_sum_le {A P : ℕ → ℝ} {C kappa omega : ℝ}
    (hC : 0 ≤ C) (hkappa : 0 ≤ kappa) (hupper : ∀ i, A i ≤ omega)
    (hbound : ∀ i, P i ≤ C * (A (i + 1) - A i + kappa * (1 / 4 : ℝ) ^ i))
    (k : ℕ) :
    (∑ i ∈ Finset.range k, P i) ≤ C * (omega - A 0 + kappa * (4 / 3)) := by
…

theorem OAI.RegularPointCoordinates.volume_defect_summable line 83

Source documentation

Comparison with the summable volume increments and curvature series proves summability of the nonnegative defects.

theorem volume_defect_summable {A P : ℕ → ℝ} {C kappa omega : ℝ}
    (hmono : Monotone A) (hupper : ∀ i, A i ≤ omega) (hP : ∀ i, 0 ≤ P i)
    (hbound : ∀ i, P i ≤ C * (A (i + 1) - A i + kappa * (1 / 4 : ℝ) ^ i)) :
    Summable P := by
…

theorem OAI.RegularPointCoordinates.volume_defect_tsum_le line 97

Source documentation

The complete defect budget depends only on the initial volume deficit and the curvature parameter.

theorem volume_defect_tsum_le {A P : ℕ → ℝ} {C kappa omega : ℝ}
    (hC : 0 ≤ C) (hkappa : 0 ≤ kappa) (hupper : ∀ i, A i ≤ omega)
    (hP : ∀ i, 0 ≤ P i)
    (hbound : ∀ i, P i ≤ C * (A (i + 1) - A i + kappa * (1 / 4 : ℝ) ^ i)) :
    (∑' i, P i) ≤ C * (omega - A 0 + kappa * (4 / 3)) := by
…

theorem OAI.RegularPointCoordinates.volume_defect_budget line 106

Source documentation

Summability and the quantitative total bound in one application.

theorem volume_defect_budget {A P : ℕ → ℝ} {C kappa omega : ℝ}
    (hC : 0 ≤ C) (hkappa : 0 ≤ kappa)
    (hmono : Monotone A) (hupper : ∀ i, A i ≤ omega) (hP : ∀ i, 0 ≤ P i)
    (hbound : ∀ i, P i ≤ C * (A (i + 1) - A i + kappa * (1 / 4 : ℝ) ^ i)) :
    Summable P ∧ (∑' i, P i) ≤ C * (omega - A 0 + kappa * (4 / 3)) :=
…

theorem OAI.RegularPointCoordinates.volume_defect_budget_of_profile_limit line 117

Source documentation

The raw Euclidean-normalized volume profile can approach its density from either side. Its convergence is enough for the same defect budget; monotonicity of that raw profile is not needed.

theorem volume_defect_budget_of_profile_limit {A P : ℕ → ℝ}
    {C kappa omega density : ℝ} (hC : 0 ≤ C)
    (hA : Tendsto A atTop (𝓝 density)) (hdensity : density ≤ omega)
    (hP : ∀ i, 0 ≤ P i)
    (hbound : ∀ i, P i ≤ C * (A (i + 1) - A i + kappa * (1 / 4 : ℝ) ^ i)) :
    Summable P ∧ (∑' i, P i) ≤ C * (omega - A 0 + kappa * (4 / 3)) := by
…

theorem OAI.RegularPointCoordinates.volume_defect_totals_tendsto_zero line 150

Source documentation

Vanishing initial volume deficit and rescaled curvature force the total nonnegative defect to vanish along a sequence of rescalings.

theorem volume_defect_totals_tendsto_zero {P : ℕ → ℕ → ℝ}
    {initialVolume kappa : ℕ → ℝ} {C omega : ℝ}
    (hvolume : Tendsto initialVolume atTop (𝓝 omega))
    (hkappa : Tendsto kappa atTop (𝓝 0)) (hP : ∀ nu i, 0 ≤ P nu i)
    (hbudget : ∀ nu, (∑' i, P nu i) ≤
      C * (omega - initialVolume nu + kappa nu * (4 / 3))) :
    Tendsto (fun nu => ∑' i, P nu i) atTop (𝓝 0) := by
…