ScaledHeatControls.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform actual heat controls before choosing the map or heat pole

theorem OAI.RegularPointCoordinates.scaled_heat_controls_at_of_splitting line 25

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 scaled_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) (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