AverageHarmonicSource.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Averaging the full harmonic cutoff source

def OAI.RegularPointCoordinates.boundedKernelAverage line 22
Source documentation
The averaged kernel is globally bounded by reciprocal testing volume. This makes it a legitimate test for a finite signed source, even at singular source poles.
```
def boundedKernelAverage {t : ℝ} (ht : 0 < t) (A : Set X)
    (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A) : X →ᵇ ℝ :=
…
```

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.average_cutoffSource line 35

Source documentation

Exact mass, curvature and cutoff-density decomposition of the actual averaged signed source. No absolute-continuity replacement of M is made.

theorem LocalHarmonicEnergy.average_cutoffSource
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hcompact : HasCompactSupport (χ : X → ℝ))
    (c : SobolevSpace μ hQ) (q : Lp ℝ 2 μ) {t : ℝ} (ht : 0 < t)
    (A : Set X) (hA : MeasurableSet A) (hbounded : Bornology.IsBounded A) :
    (∫ᵛ z, kernelAverage μ ker t A z ∂<•(G.cutoffSource μ hQ χ c q)) =
      2 * ⟪v, cutoffAverageHeatMass μ hQ hk χ.continuous hcompact M ht A hA hbounded v⟫_ℝ -
      2 * κ * (∫ z, χ z * kernelAverage μ ker t A z * localGamma μ hQ (U v) (U v) z ∂μ) +
      ∫ z, kernelAverage μ ker t A z * cutoffSourceDensity μ hQ G.energy c q z ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.cutoffAverageHeatMass, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.cutoffSourceDensity