LocalRadialDerivative.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The bounded radial derivative as a linear map into local L2

def OAI.RegularPointCoordinates.localRadialDerivative line 18
Source documentation
A locally bounded gradient defines a genuine linear derivative on Sobolev functions with values in the common local L2 space.
```
def localRadialDerivative (Ω : Set X) (f : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B) :
    SobolevSpace μ hQ →ₗ[ℝ] Lp ℝ 2 (μ.restrict Ω) where
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma
theorem OAI.RegularPointCoordinates.localRadialDerivative_representative line 40
Source documentation
The map is the original radial gradient pairing, with its slots in the customary order.
```
theorem localRadialDerivative_representative (Ω : Set X) (f q : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B) :
    localRadialDerivative μ hQ Ω f hf q =ᵐ[μ.restrict Ω] localGamma μ hQ f q :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative
theorem OAI.RegularPointCoordinates.localRadialDerivative_norm_sq line 48
Source documentation
This bound retains the local energy, so applying the derivative does not discard the scale of an already constructed radial residual.
```
theorem localRadialDerivative_norm_sq (Ω : Set X) (f q : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B) :
    ‖localRadialDerivative μ hQ Ω f hf q‖ ^ 2 ≤
      B * ∫ x in Ω, localGamma μ hQ q q x ∂μ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.localRadialDerivative
theorem OAI.RegularPointCoordinates.localRadialDerivative_eq_restrict line 69
Source documentation
Every local Sobolev representative of a radial pairing is its image under this map.
```
theorem localRadialDerivative_eq_restrict (Ω : Set X) (f q g : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hg : SobolevSpace.toLp μ hQ g =ᵐ[μ.restrict Ω] localGamma μ hQ f q) :
    localRadialDerivative μ hQ Ω f hf q = SobolevSpace.restrictLp μ hQ Ω g := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

theorem OAI.RegularPointCoordinates.localRadialDerivative_eq_of_constant_difference line 78

Source documentation

Constants in a local affine fit have zero radial derivative.

theorem localRadialDerivative_eq_of_constant_difference (Ω : Set X)
    (f q r : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B) (c : ℝ)
    (hqr : SobolevSpace.toLp μ hQ (q - r) =ᵐ[μ.restrict Ω] fun _ => c) :
    localRadialDerivative μ hQ Ω f hf q = localRadialDerivative μ hQ Ω f hf r := by
…

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