TransformedColumns.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual Sobolev columns under a coordinate transformation

def OAI.RegularPointCoordinates.transformedColumn line 19
Source documentation
The coefficient map is the adjoint of the map acting on pointwise coordinate values.
```
def transformedColumn {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (A : Euclidean n →L[ℝ] Euclidean n) : Fin n → SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.sobolevColumnMap_transformed line 24
theorem OAI.RegularPointCoordinates.transformedColumn_harmonic line 40
Source documentation
Harmonicity of the transformed scalar components follows from actual linearity in the Sobolev space.
```
theorem transformedColumn_harmonic {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (A : Euclidean n →L[ℝ] Euclidean n) (Ω : Set X)
    (hu : ∀ i, IsSobolevHarmonicOn μ hQ Ω (u i)) :
    ∀ i, IsSobolevHarmonicOn μ hQ Ω (transformedColumn μ hQ u A i) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.transformedColumn
theorem OAI.RegularPointCoordinates.meanGram_transformed_eq_id line 49
Source documentation
The exact normalization identity is the mean Gram identity for the transformed components themselves.
```
theorem meanGram_transformed_eq_id {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (A : Euclidean n ≃L[ℝ] Euclidean n) (s : Set X) (hs : MeasurableSet s)
    (hA : IsExactMeanNormalization μ hQ (sobolevColumnMap μ hQ u) s hs A) :
    sobolevMeanGram μ hQ (sobolevColumnMap μ hQ (transformedColumn μ hQ u A)) s hs =
      ContinuousLinearMap.id ℝ (Euclidean n) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.sobolevMeanGram, OAI.RegularPointCoordinates.transformedColumn