SignedSourceWeight.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The Jordan construction keeps both parts of the source, including any singular mass. No absolute continuity with respect to volume is assumed.

def OAI.RegularPointCoordinates.signedSourceWeight line 23
Source documentation
Multiply a finite signed source by a bounded continuous weight.
```
def signedSourceWeight (ν : SignedMeasure X) (χ : X →ᵇ ℝ) : SignedMeasure X :=
…
```
theorem OAI.RegularPointCoordinates.integrable_bounded_weight line 27
theorem OAI.RegularPointCoordinates.integral_signedSourceWeight line 34
Source documentation
Integration against a weighted full source is ordinary multiplication of its bounded continuous test.
```
theorem integral_signedSourceWeight (ν : SignedMeasure X) (χ w : X →ᵇ ℝ) :
    (∫ᵛ x, w x ∂<•(signedSourceWeight ν χ)) =
      ∫ᵛ x, (w * χ) x ∂<•ν := by
…
```
Mentions: OAI.RegularPointCoordinates.signedSourceWeight
theorem OAI.RegularPointCoordinates.signedSourceWeight_variation_compl line 59
Source documentation
The full variation of a weighted source vanishes off the weight's support, even when the original source has singular mass there.
```
theorem signedSourceWeight_variation_compl (ν : SignedMeasure X) (χ : X →ᵇ ℝ)
    {K : Set X} (hK : MeasurableSet K) (hχ : ∀ x ∉ K, χ x = 0) :
    (signedSourceWeight ν χ).variation Kᶜ = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.signedSourceWeight