ActualHeatEnvelope.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian upper decrement in terms of the actual Bochner envelope

def OAI.RegularPointCoordinates.dyadicHeatEnvelopeConstant line 20
Source documentation
A single constant for the shell convolution, exterior finite mass and scalar regularizer, independent of the dyadic index and vector.
```
def dyadicHeatEnvelopeConstant (M : PositiveBilinearMeasure X E) (m : ℕ)
    (A D R lambda η : ℝ) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
theorem OAI.RegularPointCoordinates.dyadicHeatEnvelopeConstant_nonneg line 28

theorem OAI.RegularPointCoordinates.gaussian_mass_budget_le_envelope line 37

Source documentation

Reindexing the Gaussian shell bound and using the finite total source gives the desired actual positive operator envelope.

theorem gaussian_mass_budget_le_envelope (M : PositiveBilinearMeasure X E)
    (m N : ℕ) (p : X) {s R A D lambda η : ℝ}
    (hs : 0 < s) (hR : (2 : ℝ) ^ N * s = R)
    (hA : 0 ≤ A) (hD : 0 < D) (hreg_nonneg : 0 ≤ lambda + η) (v : E) :
    (3 / 2 : ℝ) * (A * gaussianMassConvolutionConstant m D⁻¹ *
      (∑ j ∈ Finset.range (N + 1), (3 / 4 : ℝ) ^ j *
        (((2 ^ j * s) ^ 2 / (2 ^ j * s) ^ (m + 2)) *
          (M.measure v).real (ball p (2 ^ j * s)))) +
      s ^ 2 * ((A / s ^ (m + 2)) * Real.exp (-(4 : ℝ) ^ N / D)) *
        (M.measure v).real univ) +
      (3 / 4 : ℝ) * s ^ 2 * (lambda + η) * ‖v‖ ^ 2 ≤
    dyadicHeatEnvelopeConstant M m A D R lambda η *
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.gaussianMassConvolutionConstant, OAI.RegularPointCoordinates.dyadicHeatEnvelopeConstant

theorem OAI.RegularPointCoordinates.gaussian_dyadic_heat_increment_envelope line 99

Source documentation

The actual cutoff heat Gram satisfies the upper envelope required by the cumulative comparison, with the actual scaled Bochner mass operators.

theorem gaussian_dyadic_heat_increment_envelope (m : ℕ)
    (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {s R A D η lambda : ℝ} (hs : 0 < s) (hA : 0 ≤ A) (hD : 0 < D)
    (hη : 0 ≤ η) (hlambda0 : 0 ≤ lambda)
    (hlambda : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
    (herror : ∀ t ∈ Icc (s ^ 2 / 4) (s ^ 2), ‖harmonicHeatError μ hQ (k := ker) G χ t p‖ ≤ η)
…

Mentions: OAI.RegularPointCoordinates.harmonicHeatError