OAI/Geometry/RCD/Metric/CompactDensityTimeIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.average_density_intervalIntegrable_zero line 21

   Source documentation

   The spatial average makes any compact L1 source time-integrable at zero, using only its finite mass and the exact inverse-volume bound.

   theorem average_density_intervalIntegrable_zero (A : Set X)
       (hA : MeasurableSet A) (hAt : μ A ≠ ∞)
       {g : X → ℝ} (hg : Integrable g μ) {K : Set X} (hK : IsCompact K)
       (hz : ∀ᵐ z ∂μ, z ∉ K → g z = 0) {T : ℝ} (hT : 0 ≤ T) :
       IntervalIntegrable (fun t => ∫ z, kernelAverage μ ker t A z * g z ∂μ) volume 0 T := by
   …

   Mentions: OAI.RegularPointCoordinates.kernelAverage

2. theorem OAI.RegularPointCoordinates.difference_density_intervalIntegrable line 43

   Source documentation

   The difference pairing is integrable on every compact positive-time interval.

   theorem difference_density_intervalIntegrable (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) {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
       IntervalIntegrable (fun τ => ∫ z, (kernelAverage μ ker τ A z - ker τ x z) * g z ∂μ)
         volume s t :=
   …

   Mentions: OAI.RegularPointCoordinates.kernelAverage