RadialDyadicBudget.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Dyadic normalization of the radial mass estimate

The coefficient of the inner source mass is a fixed positive dimensional constant times the inverse power of the radius. This preserves the signed volume increments when summing; monotonicity of the raw Euclidean volume profile is not imposed.

def OAI.RegularPointCoordinates.radialCutoffCoefficient line 22
theorem OAI.RegularPointCoordinates.radialCutoffCoefficient_pos line 24
theorem OAI.RegularPointCoordinates.radialPower_height_dyadic line 28

theorem OAI.RegularPointCoordinates.radial_mass_normalized_le line 35

Source documentation

Normalize the actual annular estimate using only the outer volume bound.

theorem radial_mass_normalized_le {n r M V W curvature C : ℝ}
    (hn : 0 < n) (hr : 0 < r) (hcurvature : 0 ≤ curvature)
    (hW : W ≤ C * (2 * r) ^ n)
    (hmass : ((r ^ (-n) - (2 * r) ^ (-n)) / n) * M ≤
      r ^ (-n) * V - (2 * r) ^ (-n) * W +
      curvature * ((r ^ (-n) - (2 * r) ^ (-n)) / n) * W) :
    r ^ (-n) * M ≤ (radialCutoffCoefficient n)⁻¹ *
      (r ^ (-n) * V - (2 * r) ^ (-n) * W) + curvature * C * (2 : ℝ) ^ n := by
…

Mentions: OAI.RegularPointCoordinates.radialCutoffCoefficient

theorem OAI.RegularPointCoordinates.radial_mass_dyadic_budget line 72

Source documentation

Signed dyadic volume increments and curvature control the total normalized source mass. The density need not be attained monotonically.

theorem radial_mass_dyadic_budget {n C kappa omega density : ℝ}
    {A M : ℕ → ℝ} (hn : 0 < n)
    (hA : Tendsto A atTop (𝓝 density)) (hdensity : density ≤ omega)
    (hM : ∀ i, 0 ≤ M i)
    (hmass : ∀ i, M i ≤ (radialCutoffCoefficient n)⁻¹ * (A (i + 1) - A i) +
      kappa * (1 / 4 : ℝ) ^ i * C * (2 : ℝ) ^ n) :
    Summable M ∧ (∑' i, M i) ≤ (radialCutoffCoefficient n)⁻¹ *
      (omega - A 0 + (kappa * C * (2 : ℝ) ^ n * radialCutoffCoefficient n) * (4 / 3)) := by
…

Mentions: OAI.RegularPointCoordinates.radialCutoffCoefficient

theorem OAI.RegularPointCoordinates.radial_mass_budget_of_outer_deficit line 90

Source documentation

A uniform outer-volume deficit gives a uniform source budget, even at centers whose density is less than the Euclidean density.

theorem radial_mass_budget_of_outer_deficit {Y : Type*} {n C kappa omega delta : ℝ}
    {density : Y → ℝ} {A M : Y → ℕ → ℝ} (hn : 0 < n)
    (hA : ∀ y, Tendsto (A y) atTop (𝓝 (density y)))
    (hdensity : ∀ y, density y ≤ omega) (houter : ∀ y, omega - delta ≤ A y 0)
    (hM : ∀ y i, 0 ≤ M y i)
    (hmass : ∀ y i, M y i ≤ (radialCutoffCoefficient n)⁻¹ * (A y (i + 1) - A y i) +
      kappa * (1 / 4 : ℝ) ^ i * C * (2 : ℝ) ^ n) :
    ∀ y, Summable (M y) ∧ (∑' i, M y i) ≤
      (radialCutoffCoefficient n)⁻¹ * delta + kappa * C * (2 : ℝ) ^ n * (4 / 3) := by
…

Mentions: OAI.RegularPointCoordinates.radialCutoffCoefficient

theorem OAI.RegularPointCoordinates.radial_mass_budget_uniformly_small line 111

Source documentation

The uniform budget tends to zero along increasingly flat rescalings.

theorem radial_mass_budget_uniformly_small {Y : Type*} {n C : ℝ}
    {delta kappa : ℕ → ℝ} {M : ℕ → Y → ℕ → ℝ}
    (hdelta : Tendsto delta atTop (𝓝 0)) (hkappa : Tendsto kappa atTop (𝓝 0))
    (hbudget : ∀ ν y, (∑' i, M ν y i) ≤ (radialCutoffCoefficient n)⁻¹ * delta ν +
      kappa ν * C * (2 : ℝ) ^ n * (4 / 3)) :
    ∀ ε > 0, ∀ᶠ ν in atTop, ∀ y, (∑' i, M ν y i) < ε := by
…

Mentions: OAI.RegularPointCoordinates.radialCutoffCoefficient