OAI/Geometry/RCD/Heat/UniformHeatComparisonParameters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.exists_small_head_tail line 17

   Source documentation

   The upper bound used by the actual heat comparison, rather than just the split series itself, tends to zero with a small head and remote tail.

   theorem exists_small_head_tail {a : ℕ → ℝ} (hpos : ∀ j, 0 ≤ a j)
       {η : ℝ} (hη : 0 < η) :
       ∃ N : ℕ, ∃ ε : ℝ, 0 < ε ∧ ∀ M, N ≤ M → ∀ e, 0 ≤ e → e ≤ ε →
         e * (∑' j, a j) + ∑' j, a (j + M) < η := by
   …

2. theorem OAI.RegularPointCoordinates.uniform_heat_comparison_parameters line 37

   Source documentation

   One choice works simultaneously for all smaller radii, all later finite normalization ranges and all smaller splitting errors.

   theorem uniform_heat_comparison_parameters {a : ℕ → ℝ} (hpos : ∀ j, 0 ≤ a j)
       {C B lambda R η : ℝ} (hC : 0 ≤ C) (hη : 0 < η) :
       ∃ N : ℕ, ∃ ε : ℝ, 0 < ε ∧ ∀ k, N ≤ k → ∀ e r,
         0 ≤ e → e ≤ ε → 0 ≤ r → r ≤ 1 → (2 : ℝ) ^ k * r ≤ R →
         C * Real.exp (B * r ^ 2) *
           (e * (∑' j, a j) + ∑' j, a (j + (k + 1))) +
           |lambda * r ^ 2| * (2 : ℝ) ^ k < η := by
   …