AveragedHeatSource.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Averaged measure-source heat identity including time zero

The average of the positive kernel over a fixed finite-volume set is bounded by its reciprocal volume, uniformly at all positive times. This bounds its pairing with any finite signed measure. The genuine L2 heat flow gives continuity at zero, so the source identity extends to the initial endpoint without a pointwise kernel limit.

theorem OAI.RegularPointCoordinates.kernelAverage_bounds line 29
theorem OAI.RegularPointCoordinates.kernelAverage_eq_kernelHeat line 48
theorem OAI.RegularPointCoordinates.uniformDensityLp_integrable line 63
Source documentation
The normalized indicator is genuinely integrable on any finite-volume set, including the zero-volume case.
```
theorem uniformDensityLp_integrable (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) :
    Integrable (uniformDensityLp μ A hA hAt) μ := by
…
```
Mentions: OAI.RegularPointCoordinates.uniformDensityLp
theorem OAI.RegularPointCoordinates.kernelAverage_heatSobolev_coe line 71

theorem OAI.RegularPointCoordinates.uniformDensityLp_inner line 82

Source documentation

Pairing with the normalized indicator is exactly the actual set average.

theorem uniformDensityLp_inner (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞)
    (f : Lp ℝ 2 μ) :
    ⟪uniformDensityLp μ A hA hAt, f⟫_ℝ = (μ.real A)⁻¹ * ∫ x in A, f x ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.uniformDensityLp

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.average_heat_hasDerivAt line 91

Source documentation

The weak derivative of the average pairs the actual averaged kernel with the full signed source.

theorem IsMeasureLaplacian.average_heat_hasDerivAt
    {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 ≠ ∞)
    {t : ℝ} (ht : 0 < t) :
    HasDerivAt (fun s => ⟪heatAt μ hQ s (uniformDensityLp μ A hA hAt),
      SobolevSpace.toLp μ hQ u⟫_ℝ)
      (∫ᵛ z, kernelAverage μ p t A z ∂<•ν) t := by
…

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

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.average_heat_sub_eq_integral line 116

Source documentation

The averaged identity extends to time zero. The bound on the average kernel makes the full signed source absolutely integrable in time.

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

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.average_heat_sub_initial line 159

Source documentation

The initial-endpoint form needed for the ball Gram comparison.

theorem IsMeasureLaplacian.average_heat_sub_initial
    {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 ≠ ∞)
    {t : ℝ} (ht : 0 ≤ t) :
    (μ.real A)⁻¹ * (∫ x in A, heatAt μ hQ t (SobolevSpace.toLp μ hQ u) x ∂μ) -
      (μ.real A)⁻¹ * (∫ x in A, SobolevSpace.toLp μ hQ u x ∂μ) =
      ∫ r in 0..t, (∫ᵛ z, kernelAverage μ p r A z ∂<•ν) := by
…

theorem OAI.RegularPointCoordinates.IsMeasureLaplacian.average_initial_sub_point_heat line 176

Source documentation

Exact short/long source decomposition for comparing a ball average with a point heat value. Bounds may be applied separately to the short-time average and the long-time kernel difference; singular mass is retained.

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

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