RegularShiftedNormalizationSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Summing actual normalization errors at the interior heat scale

theorem OAI.RegularPointCoordinates.nonnegative_shifted_sum_le line 14

Source documentation

A nonnegative shifted block is bounded by its full initial segment.

theorem nonnegative_shifted_sum_le (b : ℕ → ℝ) (hb : ∀ i, 0 ≤ b i) (l k : ℕ) :
    (∑ i ∈ Finset.range k, b (l + i)) ≤ ∑ i ∈ Finset.range (l + k), b i := by
…

theorem OAI.RegularPointCoordinates.two_step_energy_sum_le line 23

Source documentation

Two-scale nonnegative increments telescope with multiplicity two.

theorem two_step_energy_sum_le (H : ℕ → ℝ) (hH : ∀ i, 0 ≤ H i)
    (hmono : Monotone H) (k : ℕ) :
    (∑ i ∈ Finset.range k, (H (i + 2) - H i)) ≤ 2 * H (k + 2) := by
…

theorem OAI.RegularPointCoordinates.regular_shifted_inverse_errors_sum_le line 46

Source documentation

The actual mean-to-interior-heat errors have one cumulative bound for any finite choice of nearby centers, with only its multiplicity as a loss.

theorem regular_shifted_inverse_errors_sum_le {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {base : X} {a κ B J C A Cχ enlargement zeta eta : ℝ}
    {ker : ℝ → X → X → ℝ}
    {hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker}
    (e : RegularProjectionEnvironment hX base hk a κ B J C A Cχ enlargement zeta eta)
    {q : X} (hq : q ∈ ball base (e.heat.radius / 32)) (hzeta : 0 ≤ zeta)
    (hsmall : (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * ((1 / 2 : ℝ) ^ n)⁻¹) * zeta) ≤ 1 / 4)
    {ι : Type*} (s : ℕ → Finset ι)
    (centers : ℕ → ι → {z : X // z ∈ ball base (e.heat.radius / 32)})
    (N : ℕ) (hcard : ∀ i, (s i).card ≤ N)
    (hroom : ∀ i y, y ∈ s i → dist (centers i y).val q ≤
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.RegularProjectionEnvironment