AverageMassEnvelope.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Shell estimates for the actual averaged Bochner heat mass

theorem OAI.RegularPointCoordinates.cutoffAverageHeatMass_integral line 22
Source documentation
Direct integration against the full positive measure; singular mass is preserved when the spatial kernel is averaged first.
```
theorem cutoffAverageHeatMass_integral (M : PositiveBilinearMeasure X E)
    {t : ℝ} (ht : 0 < t) (s : Set X) (hs : MeasurableSet s)
    (hbounded : Bornology.IsBounded s) (v : E) :
    ⟪v, cutoffAverageHeatMass μ hQ hk hχ hsχ M ht s hs hbounded v⟫_ℝ =
      ∫ z, χ z * kernelAverage μ ker t s z ∂(M.measure v) := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.cutoffAverageHeatMass, OAI.RegularPointCoordinates.kernelAverage

theorem OAI.RegularPointCoordinates.scaled_cutoffAverageHeatMass_le_geometric line 32

Source documentation

The averaged source obeys the same Gaussian shell convolution as the pointwise source, on the original full Bochner measure.

theorem scaled_cutoffAverageHeatMass_le_geometric (M : PositiveBilinearMeasure X E)
    (m : ℕ) (p : X) {r t C c T : ℝ} (hr : 0 < r) (ht : 0 < t)
    (s : Set X) (hs : MeasurableSet s) (hbounded : Bornology.IsBounded s)
    (hC : 0 ≤ C) (hc : 0 < c) (hT : 0 ≤ T) (N : ℕ)
    (hlocal : ∀ j ≤ N, ∀ z ∈ dyadicShell p r j,
      χ z * kernelAverage μ ker t s z ≤ (C / r ^ (m + 2)) * gaussianShellFactor c j)
    (htail : ∀ z ∉ ball p (2 ^ N * r), χ z * kernelAverage μ ker t s z ≤ T) (v : E) :
    r ^ 2 * ⟪v, cutoffAverageHeatMass μ hQ hk hχ hsχ M ht s hs hbounded 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)))) +
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.dyadicShell, OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.gaussianShellFactor, OAI.RegularPointCoordinates.cutoffAverageHeatMass, OAI.RegularPointCoordinates.gaussianMassConvolutionConstant