SourceTimeIntegrability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the actual compact measure sources in time

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.average_source_intervalIntegrable line 20

Source documentation

The finite signed source has an integrable averaged heat pairing, including the initial endpoint.

theorem IsMeasureLaplacian.average_source_intervalIntegrable
    {u : SobolevSpace μ hQ} {ν : SignedMeasure X}
    (hν : IsMeasureLaplacian μ hQ u ν) (c : X) {R : ℝ} (hR : 0 < R)
    (hu : ∀ᵐ x ∂μ, R < dist c x → SobolevSpace.toLp μ hQ u x = 0)
    (hsν : ν.variation (Metric.closedBall c R)ᶜ = 0)
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞)
    {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) :
    IntervalIntegrable (fun r => ∫ᵛ z, kernelAverage μ ker r A z ∂<•ν) volume s t := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.kernelAverage

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.point_source_intervalIntegrable line 54

Source documentation

The pointwise pairing with the same full source is integrable on every compact positive-time interval.

theorem IsMeasureLaplacian.point_source_intervalIntegrable
    {u : SobolevSpace μ hQ} {ν : SignedMeasure X}
    (hν : IsMeasureLaplacian μ hQ u ν) (c : X) {R : ℝ} (hR : 0 < R)
    (hu : ∀ᵐ x ∂μ, R < dist c x → SobolevSpace.toLp μ hQ u x = 0)
    (hsν : ν.variation (Metric.closedBall c R)ᶜ = 0)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) (x : X) :
    IntervalIntegrable (fun r => ∫ᵛ z, ker r x z ∂<•ν) volume s t := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp