PoissonSourceLocalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Localizing the actual distance datum and its compact-test defect

theorem OAI.RegularPointCoordinates.positiveSquaredDistance_energy_value line 18
Source documentation
For the actual positive squared-distance datum, half its energy density is the datum itself on the entire inner ball.
```
theorem positiveSquaredDistance_energy_value {p : X} {R C : ℝ} (hR : 0 ≤ R)
    (χ : GoodLaplacianCutoff μ hQ p R C)
    (heik : ∀ᵐ x ∂μ.restrict (ball p R),
      localGamma μ hQ (inwardSobolev μ hQ p R) (inwardSobolev μ hQ p R) x = 1) :
    let q := positiveSquaredDistance μ hQ hR χ
…
```
Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev, OAI.RegularPointCoordinates.positiveSquaredDistance

theorem OAI.RegularPointCoordinates.positive_defect_mono line 35

Source documentation

Compact support transfers a positive defect identity to any smaller open testing region, even when its center changes.

theorem positive_defect_mono {S T : Set X} (hST : S ⊆ T)
    (Q : SobolevSpace μ hQ) (σ : Measure X) (a : ℝ)
    (hsource : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (L : ℝ≥0),
      LipschitzWith L v → HasCompactSupport v → tsupport v ⊆ T →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
      energyForm μ hQ Q ψ + a * (∫ x in T, v x ∂μ) = ∫ x, v x ∂σ) :
    ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (L : ℝ≥0),
      LipschitzWith L v → HasCompactSupport v → tsupport v ⊆ S →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
      energyForm μ hQ Q ψ + a * (∫ x in S, v x ∂μ) = ∫ x, v x ∂σ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm