RadialLinearRepresentatives.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite radial families preserve all constant covectors

theorem OAI.RegularPointCoordinates.localRadialDerivative_column line 18
Source documentation
Once the basis radial derivatives have Sobolev representatives, their linear combinations are the radial derivatives of every coordinate covector.
```
theorem localRadialDerivative_column {n : ℕ} (Ω : Set X)
    (f : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (u g : Fin n → SobolevSpace μ hQ)
    (hg : ∀ j, SobolevSpace.toLp μ hQ (g j) =ᵐ[μ.restrict Ω] localGamma μ hQ f (u j))
    (b : Euclidean n) :
    localRadialDerivative μ hQ Ω f hf (sobolevColumnMap μ hQ u b) =
      SobolevSpace.restrictLp μ hQ Ω (sobolevColumnMap μ hQ g b) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.SobolevSpace.restrictLp
theorem OAI.RegularPointCoordinates.localRadialDerivative_constant line 32
Source documentation
The derivative kills every compactly extended local constant.
```
theorem localRadialDerivative_constant (Ω : Set X) (f q : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B) (c : ℝ)
    (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ.restrict Ω] fun _ => c) :
    localRadialDerivative μ hQ Ω f hf q = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localRadialDerivative