SourceComparisonIdentity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact average-to-point comparison with one signed source difference

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.average_initial_sub_point_heat_difference line 20

Source documentation

The exact semigroup comparison, with the long-time difference inside one integral. Both source integrals are genuinely integrable.

theorem IsMeasureLaplacian.average_initial_sub_point_heat_difference
    {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) (x : X) :
    (μ.real A)⁻¹ * (∫ z in A, SobolevSpace.toLp μ hQ u z ∂μ) -
      kernelHeat μ hQ hk s (SobolevSpace.toLp μ hQ u) x =
      ((μ.real A)⁻¹ * (∫ z in A, heatAt μ hQ t (SobolevSpace.toLp μ hQ u) z ∂μ) -
        kernelHeat μ hQ hk t (SobolevSpace.toLp μ hQ u) x) -
      (∫ r in 0..s, (∫ᵛ z, kernelAverage μ ker r A z ∂<•ν)) -
…

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