PoissonBochnerMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Full shifted Bochner mass of a Poisson replacement

The cutoff calculation keeps both the positive source measure and the full shifted Bochner measure. Its only error is the energy-density error already controlled by the linear positive-source bound.

theorem OAI.RegularPointCoordinates.poisson_bochner_mass_le line 27

Source documentation

Testing the shifted Bochner measure and the squared-distance Laplacian with the same cutoff bounds the full mass where the cutoff is one.

theorem poisson_bochner_mass_le (f : SobolevSpace μ hQ)
    (β σ : Measure X) [IsFiniteMeasure β] [IsFiniteMeasure σ]
    (χ : X →ᵇ ℝ) (hχ : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
    (s S : Set X) (hs : MeasurableSet s)
    (hχone : ∀ x ∈ s, χ x = 1)
    (Q dχ : X → ℝ) (hQi : IntegrableOn Q S μ)
    (hdχ : AEStronglyMeasurable dχ (μ.restrict S))
    {D E κ a n : ℝ} (hD : 0 ≤ D) (hκ : 0 ≤ κ) (hna : n ≤ a)
    (hdχbound : ∀ᵐ x ∂μ.restrict S, |dχ x| ≤ D)
    (herror : (∫ x in S, |(1 / 2 : ℝ) * localGamma μ hQ f f x - Q x| ∂μ) ≤ E)
    (hsource : (∫ x, χ x ∂β) =
      (1 / 2 : ℝ) * (∫ x in S, localGamma μ hQ f f x * dχ x ∂μ) +
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma