OAI/Geometry/RCD/Sobolev/CutoffSourcePairing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.average_source_components line 26

   Source documentation

   The full averaged source is the positive mass, curvature density, and actual product-rule error, with compatible representatives.

   theorem LocalHarmonicEnergy.average_source_components
       {t : ℝ} (ht : 0 < t) (A : Set X) (hA : MeasurableSet A)
       (hbounded : Bornology.IsBounded A) :
       (∫ᵛ z, kernelAverage μ ker t A z ∂<•(G.cutoffSource μ hQ χ.weight χ.sobolev χ.laplacian)) =
         2 * ⟪v, cutoffAverageHeatMassAt μ hQ hk χ.weight.continuous
           (χ.hasCompactSupport μ hQ) M A hA hbounded t v⟫_ℝ -
         2 * κ * (∫ z, kernelAverage μ ker t A z *
           (χ.weight z * localGamma μ hQ (U v) (U v) z) ∂μ) +
         ∫ 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

2. theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.difference_source_components line 46

   Source documentation

   Subtracting the pointwise source preserves the full positive-measure term and gives the kernel difference against each absolutely continuous term.

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

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