HarmonicSourceIntegral.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Integrating all three actual harmonic source components

theorem OAI.RegularPointCoordinates.integral_three_components line 14
theorem OAI.RegularPointCoordinates.curvature_integrable line 38
theorem OAI.RegularPointCoordinates.curvature_zero_off line 46

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.integrated_average_source_components line 54

Source documentation

The short-time full signed source has exactly the three integrals that have been bounded separately. Each integral is justified in L1.

theorem LocalHarmonicEnergy.integrated_average_source_components
    (A : Set X) (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A)
    {s : ℝ} (hs : 0 ≤ s) :
    (∫ t in (0 : ℝ)..s, (∫ᵛ z, kernelAverage μ ker t A z
      ∂<•(G.cutoffSource μ hQ χ.weight χ.sobolev χ.laplacian))) =
      2 * (∫ t in (0 : ℝ)..s, ⟪v, cutoffAverageHeatMassAt μ hQ hk χ.weight.continuous
        (χ.hasCompactSupport μ hQ) M A hA hbounded t v⟫_ℝ) -
      2 * κ * (∫ t in (0 : ℝ)..s, ∫ z, kernelAverage μ ker t A z *
        (χ.weight z * localGamma μ hQ (U v) (U v) z) ∂μ) +
      ∫ t in (0 : ℝ)..s, ∫ z, kernelAverage μ ker t A z *
        cutoffSourceDensity μ hQ G.energy χ.sobolev χ.laplacian z ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffAverageHeatMassAt, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.cutoffSourceDensity

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.integrated_difference_source_components line 79

Source documentation

Above the averaging scale, integration preserves the cancellation between the average and point source in every component.

theorem LocalHarmonicEnergy.integrated_difference_source_components (hρ : 0 < ρ)
    (A : Set X) (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A) (x : X)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    (∫ τ in s..t,
      (∫ᵛ z, kernelAverage μ ker τ A z ∂<•(G.cutoffSource μ hQ χ.weight χ.sobolev χ.laplacian)) -
      (∫ᵛ z, ker τ x z ∂<•(G.cutoffSource μ hQ χ.weight χ.sobolev χ.laplacian))) =
      2 * (∫ τ in s..t, ⟪v, (cutoffAverageHeatMassAt μ hQ hk χ.weight.continuous
        (χ.hasCompactSupport μ hQ) M A hA hbounded τ -
        cutoffHeatMassAt μ hQ hk χ.weight.continuous (χ.hasCompactSupport μ hQ) M τ x) v⟫_ℝ) -
      2 * κ * (∫ τ in s..t, ∫ z, (kernelAverage μ ker τ A z - ker τ x z) *
        (χ.weight z * localGamma μ hQ (U v) (U v) z) ∂μ) +
      ∫ τ in s..t, ∫ z, (kernelAverage μ ker τ A z - ker τ x z) *
…

Mentions: OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffAverageHeatMassAt, OAI.RegularPointCoordinates.cutoffHeatMassAt, OAI.RegularPointCoordinates.localGamma