SupportedAverageDifference.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Kernel differences need control only on the fixed cutoff support

theorem OAI.RegularPointCoordinates.cutoffAverageHeatMass_difference_le_supported line 21

Source documentation

An all-pole kernel bound on the cutoff support suffices for the full positive source measure. No volume bounds are required away from that support.

theorem cutoffAverageHeatMass_difference_le_supported
    (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, χ z ≠ 0 → |kernelAverage μ ker t s z - ker t x z| ≤ B z)
    (v : E) :
    |⟪v, (cutoffAverageHeatMass μ hQ hk hχ hsχ M ht s hs hbounded -
      cutoffHeatMass μ hQ hk 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