KernelMeasureBounds.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Continuous kernel bounds at every source pole

Bounds initially valid almost everywhere in the reference measure extend to every pole by continuity and full support. The resulting pointwise bounds may then be integrated against a singular local mass measure.

def OAI.RegularPointCoordinates.kernelAverage line 28
Source documentation
An actual average over the testing set, in the first kernel variable.
```
def kernelAverage (p : ℝ → X → X → ℝ) (t : ℝ) (s : Set X) (z : X) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.kernelAverage_continuous line 32
theorem OAI.RegularPointCoordinates.continuous_bound_everywhere line 61
Source documentation
Full support turns a continuous almost-everywhere inequality into an everywhere inequality. The measure used for this extension is the reference measure, not the possibly singular measure used afterwards.
```
theorem continuous_bound_everywhere [μ.IsOpenPosMeasure]
    {f g : X → ℝ} (hf : Continuous f) (hg : Continuous g)
    (h : ∀ᵐ z ∂μ, f z ≤ g z) : ∀ z, f z ≤ g z := by
…
```

theorem OAI.RegularPointCoordinates.kernelAverage_difference_everywhere line 76

Source documentation

The averaged kernel difference estimate extends to every pole before it is paired with the full Bochner measure.

theorem kernelAverage_difference_everywhere [IsLocallyFiniteMeasure μ]
    [μ.IsOpenPosMeasure] {t : ℝ} (ht : 0 < t) {s : Set X}
    (hs : MeasurableSet s) (hbounded : Bornology.IsBounded s) (x : X)
    (B : X → ℝ) (hB : Continuous B)
    (h : ∀ᵐ z ∂μ, |kernelAverage μ p t s z - p t x z| ≤ B z) :
    ∀ z, |kernelAverage μ p t s z - p t x z| ≤ B z :=
…

Mentions: OAI.RegularPointCoordinates.kernelAverage

theorem OAI.RegularPointCoordinates.compact_weight_bound line 87
def OAI.RegularPointCoordinates.compactWeight line 92

def OAI.RegularPointCoordinates.cutoffAverageHeatMass line 102

Source documentation

Average the kernel first, then integrate the cutoff average against the full mass measure.

def cutoffAverageHeatMass {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (M : PositiveBilinearMeasure X E) {t : ℝ} (ht : 0 < t)
    (s : Set X) (hs : MeasurableSet s) (hbounded : Bornology.IsBounded s) : E →L[ℝ] E :=
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure

theorem OAI.RegularPointCoordinates.cutoffAverageHeatMass_energy line 112

Source documentation

Fubini identifies integration of the averaged kernel with the average of the actual heat mass matrices. Compact cutoffs control the integrand even when the mass is singular.

theorem cutoffAverageHeatMass_energy {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (M : PositiveBilinearMeasure X E) {t : ℝ} (ht : 0 < t)
    (s : Set X) (hs : MeasurableSet s) (hbounded : Bornology.IsBounded s) (v : E) :
    ⟪v, cutoffAverageHeatMass μ hQ hp hχ hsχ M ht s hs hbounded v⟫_ℝ =
      (μ.real s)⁻¹ * ∫ a in s, ⟪v, cutoffHeatMass μ hQ hp hχ hsχ M ht a v⟫_ℝ ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.cutoffAverageHeatMass_difference_le line 156

Source documentation

The continuous all-pole extension permits the kernel difference to be integrated against singular mass, with its full quantitative bound.

theorem cutoffAverageHeatMass_difference_le {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    [μ.IsOpenPosMeasure] (M : PositiveBilinearMeasure X E)
    (hχpos : ∀ z, 0 ≤ χ z) {t : ℝ} (ht : 0 < t)
    (s : Set X) (hs : MeasurableSet s) (hbounded : Bornology.IsBounded s) (x : X)
    (B : X → ℝ) (hB : Continuous B)
    (hbound : ∀ᵐ z ∂μ, |kernelAverage μ p t s z - p t x z| ≤ B z) (v : E) :
    |⟪v, (cutoffAverageHeatMass μ hQ hp hχ hsχ M ht s hs hbounded -
      cutoffHeatMass μ hQ hp hχ hsχ M ht x) v⟫_ℝ| ≤
      ∫ z, χ z * B z ∂(M.measure v) := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffAverageHeatMass, OAI.RegularPointCoordinates.cutoffHeatMass

theorem OAI.RegularPointCoordinates.cutoffAverageHeatMass_difference_bilinear_le line 182

Source documentation

The actual averaged-minus-pointwise heat mass satisfies the bilinear bound in the same full Bochner measure, including its singular part.

theorem cutoffAverageHeatMass_difference_bilinear_le {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    [μ.IsOpenPosMeasure] (M : PositiveBilinearMeasure X E)
    (hχpos : ∀ z, 0 ≤ χ z) {t : ℝ} (ht : 0 < t)
    (s : Set X) (hs : MeasurableSet s) (hbounded : Bornology.IsBounded s) (x : X)
    (B : X → ℝ) (hB : Continuous B)
    (hbound : ∀ᵐ z ∂μ, |kernelAverage μ p t s z - p t x z| ≤ B z) (v w : E) :
    ⟪v, (cutoffAverageHeatMass μ hQ hp hχ hsχ M ht s hs hbounded -
      cutoffHeatMass μ hQ hp hχ hsχ M ht x) w⟫_ℝ ^ 2 ≤
      (∫ z, χ z * B z ∂(M.measure v)) * (∫ z, χ z * B z ∂(M.measure w)) := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffAverageHeatMass, OAI.RegularPointCoordinates.cutoffHeatMass