DyadicHeatFamily.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual dyadic heat Gram equivalences and their two decrement bounds

theorem OAI.RegularPointCoordinates.dyadic_radius_square_succ line 15
def OAI.RegularPointCoordinates.dyadicHeatGram line 29
Source documentation
All dyadic heat metrics are the actual regularized heat Grams of one fixed coordinate span, cutoff and pole.
```
def dyadicHeatGram {R lambda : ℝ} (hR : 0 < R) (hlambda : 0 < lambda) (i : ℕ) :
    Euclidean n ≃L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.cutoffHeatGram_time_congr line 35
theorem OAI.RegularPointCoordinates.dyadicHeatGram_coe line 42
theorem OAI.RegularPointCoordinates.dyadicHeatGram_isPositive line 47

theorem OAI.RegularPointCoordinates.dyadicHeatGram_lower line 57

Source documentation

The lower decrement controls exactly the dyadic full Bochner mass.

theorem dyadicHeatGram_lower (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 p (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 p‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError

theorem OAI.RegularPointCoordinates.dyadicHeatGram_upper line 83

Source documentation

The upper decrement has the same fixed-root mass envelope at every index, with one constant independent of the index and direction.

theorem dyadicHeatGram_upper (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 : ℕ)
    (herror : ∀ t ∈ Icc ((R / 2 ^ i) ^ 2 / 4) ((R / 2 ^ i) ^ 2),
      ‖harmonicHeatError μ hQ (k := ker) G χ t p‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError