DyadicHeatAt.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

One fixed cutoff and the actual dyadic heat metrics at nearby poles

def OAI.RegularPointCoordinates.dyadicHeatGramAt line 22
Source documentation
The cutoff remains fixed while the heat pole varies.
```
def dyadicHeatGramAt (x : X) {R lambda : ℝ} (hR : 0 < R) (hlambda : 0 < lambda) (i : ℕ) :
    Euclidean n ≃L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.dyadicHeatGramAt_coe line 28
theorem OAI.RegularPointCoordinates.dyadicHeatGramAt_isPositive line 33
theorem OAI.RegularPointCoordinates.cutoffHeatGram_time_congr_at line 39

theorem OAI.RegularPointCoordinates.dyadicHeatGramAt_lower line 50

Source documentation

The lower mass bound also remains centered at the heat pole.

theorem dyadicHeatGramAt_lower (x : X) (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {R c η lambda : ℝ} (hR : 0 < R) (hlambda : 0 < lambda)
    (hreg : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda) (i : ℕ)
    (hχone : ∀ y ∈ ball x (R / 2 ^ i), (χ.weight : X → ℝ) y = 1)
    (herror : ∀ t ∈ Icc ((R / 2 ^ i) ^ 2 / 4) ((R / 2 ^ i) ^ 2),
      ‖harmonicHeatError μ hQ (k := ker) G χ t x‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError

theorem OAI.RegularPointCoordinates.dyadicHeatGramAt_upper_supported line 79

Source documentation

The upper mass envelope is centered at the pole, independently of the center of the one fixed cutoff.

theorem dyadicHeatGramAt_upper_supported (x : X) (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 x R, (χ.weight : X → ℝ) z = 0)
    (herror : ∀ t ∈ Icc ((R / 2 ^ i) ^ 2 / 4) ((R / 2 ^ i) ^ 2),
      ‖harmonicHeatError μ hQ (k := ker) G χ t x‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError