HeatMassTimeContinuity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Positive-time continuity and integrability of full heat mass

theorem OAI.RegularPointCoordinates.cutoffHeatMassAt_continuousOn line 23
Source documentation
The finite positive Bochner measure may be singular; continuity follows from the actual joint kernel and the fixed compact cutoff.
```
theorem cutoffHeatMassAt_continuousOn (M : PositiveBilinearMeasure X E) (x : X) (v : E) :
    ContinuousOn (fun t => ⟪v, cutoffHeatMassAt μ hQ hk hχ hc M t x v⟫_ℝ) (Ioi 0) := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.cutoffHeatMassAt
theorem OAI.RegularPointCoordinates.cutoffAverageHeatMassAt_continuousOn line 39
Source documentation
Averaging in the first pole preserves the same positive-time continuity against the full Bochner measure.
```
theorem cutoffAverageHeatMassAt_continuousOn (M : PositiveBilinearMeasure X E)
    (A : Set X) (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A) (v : E) :
    ContinuousOn (fun t => ⟪v, cutoffAverageHeatMassAt μ hQ hk hχ hc M A hA hbounded t v⟫_ℝ)
      (Ioi 0) := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.cutoffAverageHeatMassAt

theorem OAI.RegularPointCoordinates.cutoffAverageHeatMassAt_difference_intervalIntegrable line 56

Source documentation

Both terms in a long-time block are genuinely integrable.

theorem cutoffAverageHeatMassAt_difference_intervalIntegrable
    (M : PositiveBilinearMeasure X E) (A : Set X) (hA : MeasurableSet A)
    (hbounded : Bornology.IsBounded A) (x : X) (v : E)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    IntervalIntegrable (fun r => ⟪v, (cutoffAverageHeatMassAt μ hQ hk hχ hc M A hA hbounded r -
      cutoffHeatMassAt μ hQ hk hχ hc M r x) v⟫_ℝ) volume s t := by
…

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