RadialDerivativeNorms.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual radial derivative errors in the common normalized L2 space

theorem OAI.RegularPointCoordinates.normalized_radial_derivative_norm_sq line 19
Source documentation
The derivative's local energy estimate passes directly to normalized L2, including the original volume denominator.
```
theorem normalized_radial_derivative_norm_sq (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (f q : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B) :
    ‖normalizeLocalL2 μ Ω hfin (localRadialDerivative μ hQ Ω f hf q)‖ ^ 2 ≤
      B * (μ.real Ω)⁻¹ * ∫ x in Ω, localGamma μ hQ q q x ∂μ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.localRadialDerivative

theorem OAI.RegularPointCoordinates.local_radial_commutator_norm_sq line 31

Source documentation

The squared L2 norm of the algebraic commutator is exactly the integral controlled by the full Poisson mass estimate.

theorem local_radial_commutator_norm_sq (Ω : Set X)
    (f v u g h : SobolevSpace μ hQ) {Cf Cv : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ Cf)
    (hv : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ v v x ≤ Cv)
    (hh : SobolevSpace.toLp μ hQ h =ᵐ[μ.restrict Ω] localGamma μ hQ v u) :
    ‖localRadialDerivative μ hQ Ω v hv g - localRadialDerivative μ hQ Ω f hf h -
      SobolevSpace.restrictLp μ hQ Ω h‖ ^ 2 =
    ∫ x in Ω, (localGamma μ hQ v g x - localGamma μ hQ f h x - localGamma μ hQ v u x) ^ 2 ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp