BochnerCutoffIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The canonical Bochner cutoff identity from local measure calculus

theorem OAI.RegularPointCoordinates.integral_harmonicBochnerSource line 20
Source documentation
Integrating the actual full Bochner source retains its singular part.
```
theorem integral_harmonicBochnerSource (U : E →L[ℝ] SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X E) (κ : ℝ) (v : E) (χ : X →ᵇ ℝ) :
    (∫ᵛ x, χ x ∂<•(harmonicBochnerSource μ hQ U M κ v)) =
      2 * ⟪v, M.weightedOperator χ v⟫_ℝ -
        2 * κ * ∫ x, χ x * localGamma μ hQ (U v) (U v) x ∂μ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.harmonicBochnerSource, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.test_cutoff line 39

Source documentation

The local Bochner equation and the weak Laplacian of the cutoff give the precise mass identity used by bochner_mass_le_of_local_error.

theorem LocalHarmonicEnergy.test_cutoff
    {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
    {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0} {v : E}
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχs : HasCompactSupport (χ : X → ℝ))
    (hχΩ : tsupport (χ : X → ℝ) ⊆ ball p (2 * r))
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (q : Lp ℝ 2 μ) (hq : IsWeakLaplacian μ hQ c q)
    (hqs : ∀ᵐ x ∂μ, x ∉ ball p (2 * r) → q x = 0) :
    ⟪v, M.weightedOperator χ v⟫_ℝ =
      (1 / 2 : ℝ) * (∫ x, localGamma μ hQ (U v) (U v) x * q x ∂μ) +
        κ * ∫ x, χ x * localGamma μ hQ (U v) (U v) x ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.localGamma