FiniteHeatMassShells.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite shell bounds for the full Bochner heat mass

theorem OAI.RegularPointCoordinates.finite_dyadicShell_union line 19
Source documentation
The first N+1 shells partition exactly the corresponding outer ball.
```
theorem finite_dyadicShell_union (p : X) {r : ℝ} (hr : 0 ≤ r) (N : ℕ) :
    (⋃ j ∈ Finset.range (N + 1), dyadicShell p r j) = ball p (2 ^ N * r) := by
…
```
Mentions: OAI.RegularPointCoordinates.dyadicShell

theorem OAI.RegularPointCoordinates.integral_le_finite_shell_mass line 30

Source documentation

Integrate finitely many controlled shells and use a single bound on the exterior. This applies directly to singular finite mass measures.

theorem integral_le_finite_shell_mass (ν : Measure X) [IsFiniteMeasure ν]
    (p : X) {r : ℝ} (hr : 0 ≤ r) (N : ℕ) {f : X → ℝ} (hf : Integrable f ν)
    (W : ℕ → ℝ) (hW : ∀ j, 0 ≤ W j)
    (hlocal : ∀ j ≤ N, ∀ᵐ z ∂ν.restrict (dyadicShell p r j), f z ≤ W j)
    {T : ℝ} (hT : 0 ≤ T)
    (htail : ∀ᵐ z ∂ν.restrict (ball p (2 ^ N * r))ᶜ, f z ≤ T) :
    (∫ z, f z ∂ν) ≤
      (∑ j ∈ Finset.range (N + 1), W j * ν.real (ball p (2 ^ j * r))) + T * ν.real univ := by
…

Mentions: OAI.RegularPointCoordinates.dyadicShell

theorem OAI.RegularPointCoordinates.cutoffHeatMass_le_finite_shells line 63

Source documentation

The shell bound controls the actual heat mass of the full positive Bochner measure, not just an assumed density.

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

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