ColumnRepresentatives.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise representatives of the actual affine coordinate changes

theorem OAI.RegularPointCoordinates.sobolevColumnMap_representative line 18
Source documentation
A Sobolev linear combination represents the corresponding scalar pairing with the pointwise coordinate vector.
```
theorem sobolevColumnMap_representative {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (s : Set X) (v : X → Euclidean n)
    (hu : ∀ i, SobolevSpace.toLp μ hQ (u i) =ᵐ[μ.restrict s] fun x => v x i)
    (a : Euclidean n) :
    SobolevSpace.toLp μ hQ (sobolevColumnMap μ hQ u a) =ᵐ[μ.restrict s]
      fun x => ⟪v x, a⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.affineChangedColumn_representative line 45

Source documentation

Adding a compact local constant to transformed Sobolev columns gives exactly the affine change of their pointwise vector representative.

theorem affineChangedColumn_representative {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (s : Set X) (v : X → Euclidean n)
    (hu : ∀ i, SobolevSpace.toLp μ hQ (u i) =ᵐ[μ.restrict s] fun x => v x i)
    (B : Euclidean n →L[ℝ] Euclidean n) (b : Euclidean n →L[ℝ] ℝ)
    (η : SobolevSpace μ hQ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict s] fun _ => (1 : ℝ)) (i : Fin n) :
    SobolevSpace.toLp μ hQ (affineChangedColumn μ hQ u B b η i) =ᵐ[μ.restrict s]
      fun x => (B.adjoint (v x)) i + b (EuclideanSpace.single i 1) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.affineChangedColumn