AveragedDensityFubini.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Fubini for the actual compact integrable cutoff errors

theorem OAI.RegularPointCoordinates.kernelAverage_integral_density line 20

Source documentation

Averaging and integration commute for the genuine integrable compact error density, even when it is not an L2 function.

theorem kernelAverage_integral_density {t : ℝ} (ht : 0 < t)
    (A : Set X) (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A)
    {g : X → ℝ} (hg : Integrable g μ) {K : Set X} (hK : IsCompact K)
    (hgzero : ∀ᵐ z ∂μ, z ∉ K → g z = 0) :
    (∫ z, kernelAverage μ ker t A z * g z ∂μ) =
      (μ.real A)⁻¹ * ∫ y in A, ∫ z, ker t y z * g z ∂μ ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.kernelAverage