RadialDerivativeError.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The radial derivative error from the actual Poisson energy error

theorem OAI.RegularPointCoordinates.localGamma_sq_le line 18
theorem OAI.RegularPointCoordinates.localGamma_memLp_two_of_bound line 30
Source documentation
A bounded gradient in the second slot makes its pairing with every Sobolev gradient locally square-integrable.
```
theorem localGamma_memLp_two_of_bound (Ω : Set X) (f a : SobolevSpace μ hQ)
    {B : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ a a x ≤ B) :
    MemLp (localGamma μ hQ f a) 2 (μ.restrict Ω) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.radial_pairing_error_le line 45

Source documentation

The raw radial derivative changes by at most the bounded coordinate gradient times the Poisson energy error.

theorem radial_pairing_error_le (Ω : Set X) (q f a : SobolevSpace μ hQ)
    {B : ℝ}
    (ha : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ a a x ≤ B) :
    (∫ x in Ω, (localGamma μ hQ q a x - localGamma μ hQ f a x) ^ 2 ∂μ) ≤
      B * ∫ x in Ω, localGamma μ hQ (q - f) (q - f) x ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.radial_pairing_error_le_source line 65

Source documentation

The source estimate gives a linear, not square-root, bound for the squared radial derivative error.

theorem radial_pairing_error_le_source (Ω : Set X) (hΩ : MeasurableSet Ω)
    (hfin : μ Ω ≠ ∞) (q a : SobolevSpace μ hQ)
    (H : SobolevSpace.dirichlet μ hQ Ω) (σ : Measure X) [IsFiniteMeasure σ]
    (hsource : IsDirichletMeasureSource μ hQ Ω H.val σ)
    {d C B A : ℝ} (hd : 1 < d) (hC : 0 ≤ C) (hB : 0 ≤ B) (hA : 0 ≤ A)
    (hheight : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x ∧
      SobolevSpace.toLp μ hQ H.val x ≤ B)
    (ha : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ a a x ≤ A)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val) :
    (∫ x in Ω, (localGamma μ hQ q a x - localGamma μ hQ (q - H.val) a x) ^ 2 ∂μ) ≤
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.IsDirichletMeasureSource, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.energyForm