OAI/Geometry/RCD/Metric/AverageMassInitial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the averaged positive source at the initial time

  1. theorem OAI.RegularPointCoordinates.cutoffAverageHeatMassAt_intervalIntegrable_zero line 21

    Source documentation

    Averaging makes the full finite positive source integrable down to zero time. The bound uses unit heat mass and retains singular source mass.

    theorem cutoffAverageHeatMassAt_intervalIntegrable_zero
    (M : PositiveBilinearMeasure X E) (hχbounds : ∀ z, 0 ≤ χ z ∧ χ z ≤ 1)
    (A : Set X) (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A)
    (v : E) {T : ℝ} (hT : 0 ≤ T) :
    IntervalIntegrable (fun t => ⟪v, cutoffAverageHeatMassAt μ hQ hk hχ hc M A hA hbounded t v⟫_ℝ)
      volume 0 T := by
…

    Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.cutoffAverageHeatMassAt