OAI/Geometry/RCD/Heat/KernelDensityTime.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.integral_compact_density_continuousOn_time line 19

   Source documentation

   Compact L1 support is sufficient for positive-time continuity of the source pairing, for both the kernel and its actual spatial average.

   theorem integral_compact_density_continuousOn_time
       {k : ℝ × X → ℝ} (hc : ContinuousOn k (Ioi 0 ×ˢ univ))
       {g : X → ℝ} (hg : Integrable g μ) {K : Set X} (hK : IsCompact K)
       (hz : ∀ᵐ z ∂μ, z ∉ K → g z = 0) :
       ContinuousOn (fun t => ∫ z, k (t, z) * g z ∂μ) (Ioi 0) := by
   …

2. theorem OAI.RegularPointCoordinates.kernel_density_continuousOn_time line 64
3. theorem OAI.RegularPointCoordinates.average_density_continuousOn_time line 71
4. theorem OAI.RegularPointCoordinates.difference_density_continuousOn_time line 81

   Source documentation

   The compact L1 source also gives a continuous averaged difference pairing.

   theorem difference_density_continuousOn_time (A : Set X)
       (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A) (x : X)
       {g : X → ℝ} (hg : Integrable g μ) {K : Set X} (hK : IsCompact K)
       (hz : ∀ᵐ z ∂μ, z ∉ K → g z = 0) :
       ContinuousOn (fun t => ∫ z, (kernelAverage μ ker t A z - ker t x z) * g z ∂μ) (Ioi 0) := by
   …

   Mentions: OAI.RegularPointCoordinates.kernelAverage