LocalDensitySource.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Local replacement of the absolutely continuous source

theorem OAI.RegularPointCoordinates.IsMeasureLaplacianOn.sourceDensity_congr line 18
theorem OAI.RegularPointCoordinates.localGamma_constant_source line 43
Source documentation
A locally constant Sobolev source has zero gradient pairing there.
```
theorem localGamma_constant_source {Ω : Set X}
    (f d : SobolevSpace μ hQ) (c : ℝ)
    (hd : SobolevSpace.toLp μ hQ d =ᵐ[μ.restrict Ω] fun _ => c) :
    localGamma μ hQ f d =ᵐ[μ.restrict Ω] fun _ => 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.IsMeasureLaplacianOn.bochner_constant_source line 53

Source documentation

Constant local sources remove both derivative terms in the Bochner Gram equation, even for compact extensions of the original potential.

theorem IsMeasureLaplacianOn.bochner_constant_source {Ω : Set X} (hΩ : MeasurableSet Ω)
    (K : ℝ) (F f f' d : SobolevSpace μ hQ) (c : ℝ) (σ : SignedMeasure X)
    (hF : IsMeasureLaplacianOn μ hQ Ω F
      ((2:ℝ) • σ+μ.withDensityᵥ (fun x => 2*K*localGamma μ hQ f f x)))
    (hff : SobolevSpace.toLp μ hQ f' =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ f)
    (hd : SobolevSpace.toLp μ hQ d =ᵐ[μ.restrict Ω] fun _ => c) :
    IsMeasureLaplacianOn μ hQ Ω F (bochnerGramSource μ hQ K f' f' d d σ) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsMeasureLaplacianOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.bochnerGramSource

theorem OAI.RegularPointCoordinates.IsMeasureLaplacianOn.bochner_constant_source_shifted line 68