ScaledHeatMassShells.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual scaled heat mass is controlled by a geometric ball-mass convolution

theorem OAI.RegularPointCoordinates.scaled_cutoffHeatMass_le_geometric line 23

Source documentation

Gaussian shell bounds give the geometric convolution in the actual ball masses, plus only the explicit exterior contribution.

theorem scaled_cutoffHeatMass_le_geometric (M : PositiveBilinearMeasure X E)
    (m : ℕ) (p : X) {r t C c T : ℝ} (hr : 0 < r) (ht : 0 < t)
    (hC : 0 ≤ C) (hc : 0 < c) (hT : 0 ≤ T) (N : ℕ)
    (hlocal : ∀ j ≤ N, ∀ z ∈ dyadicShell p r j,
      χ z * ker t p z ≤ (C / r ^ (m + 2)) * gaussianShellFactor c j)
    (htail : ∀ z ∉ ball p (2 ^ N * r), χ z * ker t p z ≤ T) (v : E) :
    r ^ 2 * ⟪v, cutoffHeatMass μ hQ hk hχ hsχ M ht p v⟫_ℝ ≤
      C * gaussianMassConvolutionConstant m c *
        (∑ j ∈ Finset.range (N + 1), (3 / 4 : ℝ) ^ j *
          (((2 ^ j * r) ^ 2 / (2 ^ j * r) ^ (m + 2)) *
            (M.measure v).real (ball p (2 ^ j * r)))) +
      r ^ 2 * T * (M.measure v).real univ := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.dyadicShell, OAI.RegularPointCoordinates.gaussianShellFactor, OAI.RegularPointCoordinates.cutoffHeatMass, OAI.RegularPointCoordinates.gaussianMassConvolutionConstant