OAI/Geometry/RCD/Heat/KernelDensityContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.continuous_mul_integrable_compact line 19

   Source documentation

   A continuous multiplier preserves integrability of a compact L1 density.

   theorem continuous_mul_integrable_compact {k g : X → ℝ} (hc : Continuous k)
       (hg : Integrable g μ) {K : Set X} (hK : IsCompact K)
       (hz : ∀ᵐ z ∂μ, z ∉ K → g z = 0) : Integrable (fun z => k z * g z) μ := by
   …

2. theorem OAI.RegularPointCoordinates.kernel_integral_density_continuous line 36

   Source documentation

   Compact L1 densities give continuous positive-time heat pairings. This applies to the cutoff error without requiring it to belong to L2.

   theorem kernel_integral_density_continuous {t : ℝ} (ht : 0 < t)
       {g : X → ℝ} (hg : Integrable g μ) {K : Set X} (hK : IsCompact K)
       (hgzero : ∀ᵐ z ∂μ, z ∉ K → g z = 0) :
       Continuous (fun y => ∫ z, ker t y z * g z ∂μ) := by
   …