CenteredColumns.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual Sobolev columns after a linear change and local recentering

theorem OAI.RegularPointCoordinates.sobolevColumnMap_of_linear line 19
Source documentation
A continuous linear Sobolev family is recovered from its finite standard coordinate columns.
```
theorem sobolevColumnMap_of_linear {n : ℕ}
    (U : Euclidean n →L[ℝ] SobolevSpace μ hQ) :
    sobolevColumnMap μ hQ (fun i => U (EuclideanSpace.single i 1)) = U := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.sobolevColumnMap
def OAI.RegularPointCoordinates.affineChangedColumn line 31
Source documentation
The local constant is supplied by a genuine compact Sobolev cutoff.
```
def affineChangedColumn {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (B : Euclidean n →L[ℝ] Euclidean n) (b : Euclidean n →L[ℝ] ℝ)
    (η : SobolevSpace μ hQ) : Fin n → SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.sobolevColumnMap_affineChanged line 37
theorem OAI.RegularPointCoordinates.affineChangedColumn_residual_eq line 46
Source documentation
Recentring and normalizing the actual Sobolev columns preserves their least-squares residual on every set where the cutoff equals one.
```
theorem affineChangedColumn_residual_eq {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (B : Euclidean n ≃L[ℝ] Euclidean n) (b : Euclidean n →L[ℝ] ℝ)
    (η : SobolevSpace μ hQ) (s : Set X) (hfin : μ s ≠ ∞)
    (hη : SobolevSpace.restrictLp μ hQ s η = restrictedOne μ s hfin) :
    affineResidual μ hQ (affineChangedColumn μ hQ u B b η) s hfin =
      affineResidual μ hQ u s hfin := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.restrictedOne, OAI.RegularPointCoordinates.affineResidual, OAI.RegularPointCoordinates.affineChangedColumn
theorem OAI.RegularPointCoordinates.restrictLp_eq_one_of_representative line 60
Source documentation
A local pointwise representative equal to one identifies the restriction with the constant generator of the affine space.
```
theorem restrictLp_eq_one_of_representative (η : SobolevSpace μ hQ)
    (s : Set X) (hfin : μ s ≠ ∞)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict s] fun _ => (1 : ℝ)) :
    SobolevSpace.restrictLp μ hQ s η = restrictedOne μ s hfin := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.restrictedOne