UniformHeatControlsAt.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform actual heat controls before choosing the map or heat pole

theorem OAI.RegularPointCoordinates.uniform_heat_controls_at_of_splitting line 24

Source documentation

One tolerance, decrement constant and comparison index work for all maps and poles satisfying the displayed geometric bounds. The cutoff may be fixed independently of the evaluation pole.

theorem uniform_heat_controls_at_of_splitting {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 2) X) (comparisonModelVolume (m + 1) a))
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff (m + 2) X) hX.quadratic ker)
    (hg : HasCoordinateHeatBounds (hausdorff (m + 2) X) ker)
    {L B Vlo Vhi C η lambda : ℝ} (hL : 0 ≤ L) (hB : 0 ≤ B)
    (hVlo : 0 < Vlo) (hVhi : 0 < Vhi) (hC : 0 ≤ C) (hη : 0 ≤ η) (hlambda : 0 < lambda) :
    ∃ ε εmass C₁ : ℝ, ∃ N : ℕ,
      0 < ε ∧ ε ≤ 1 ∧ 0 ≤ εmass ∧ 0 ≤ C₁ ∧
      2 * C₁ * (2 * geometricIntervalConstant ((3 / 4 : ℝ) * (9 / 8))) * εmass ≤ 1 / 2 ∧
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.geometricIntervalConstant