SupportedHeatEnvelope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A supported heat envelope with no exterior mass constant

def OAI.RegularPointCoordinates.supportedHeatEnvelopeConstant line 16
Source documentation
The supported upper-decrement constant has no dependence on the total Bochner mass outside the working ball.
```
def supportedHeatEnvelopeConstant (m : ℕ) (A D R lambda η : ℝ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.supportedHeatEnvelopeConstant_nonneg line 20

theorem OAI.RegularPointCoordinates.dyadicHeatGram_upper_supported line 38

Source documentation

With cutoff support inside the fixed outer ball, the exterior term vanishes exactly. The actual upper heat decrement then has a constant depending only on Gaussian bounds, scale and regularization.

theorem dyadicHeatGram_upper_supported (m : ℕ) (hn : n = m + 2)
    (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {R A D η lambda : ℝ} (hR : 0 < R) (hlambda : 0 < lambda)
    (hA : 0 ≤ A) (hD : 0 < D) (hη : 0 ≤ η)
    (hreg : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda) (i : ℕ)
    (hχzero : ∀ z ∉ ball p R, (χ.weight : X → ℝ) z = 0)
    (herror : ∀ t ∈ Icc ((R / 2 ^ i) ^ 2 / 4) ((R / 2 ^ i) ^ 2),
      ‖harmonicHeatError μ hQ (k := ker) G χ t p‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError