EventualDyadicHeatCumulative.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Cumulative comparison for the actual heat family at small scales

theorem OAI.RegularPointCoordinates.eventual_dyadic_heat_cumulative_comparison line 25

Source documentation

No heat or small-mass bounds at the omitted coarse scales are needed. In particular the cutoff may transition between the root ball and its quarter ball, while all terms remain those of the original coordinate map.

theorem eventual_dyadic_heat_cumulative_comparison {R lambda ε C : ℝ}
    (hR : 0 < R) (hlambda : 0 < lambda) (hε : 0 ≤ ε) (hC : 0 ≤ C) (J : ℕ)
    (hstep : ∀ i, J ≤ i → ∀ v, ⟪v, dyadicHeatGram μ hQ hk U χ hR hlambda i v⟫_ℝ ≤
      (9 / 8 : ℝ) * ⟪v, dyadicHeatGram μ hQ hk U χ hR hlambda (i + 1) v⟫_ℝ)
    (hdecrement : ∀ i, J ≤ i → ∀ v,
      let d := ⟪v, ((dyadicHeatGram μ hQ hk U χ hR hlambda i : Euclidean n →L[ℝ] Euclidean n) -
…

Mentions: OAI.RegularPointCoordinates.dyadicHeatGram, OAI.RegularPointCoordinates.Euclidean