AffineChange.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Least-squares affine fits are independent of coordinate normalization

theorem OAI.RegularPointCoordinates.affineCoordinateSpace_eq_of_change line 18
Source documentation
An invertible linear coordinate change and a translation by constants preserve the actual finite-dimensional affine subspace in local L².
```
theorem affineCoordinateSpace_eq_of_change {n : ℕ}
    (u u' : Fin n → SobolevSpace μ hQ) (s : Set X) (hfin : μ s ≠ ∞)
    (B : Euclidean n ≃L[ℝ] Euclidean n) (b : Euclidean n →L[ℝ] ℝ)
    (hchange : ∀ v, SobolevSpace.restrictLp μ hQ s (sobolevColumnMap μ hQ u' v) =
      SobolevSpace.restrictLp μ hQ s (sobolevColumnMap μ hQ u (B v)) +
        b v • restrictedOne μ s hfin) :
    affineCoordinateSpace μ hQ u' s hfin = affineCoordinateSpace μ hQ u s hfin := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.restrictedOne, OAI.RegularPointCoordinates.affineCoordinateSpace

theorem OAI.RegularPointCoordinates.affineProjection_eq_of_change line 45

Source documentation

Consequently the least-squares projection itself is unchanged.

theorem affineProjection_eq_of_change {n : ℕ}
    (u u' : Fin n → SobolevSpace μ hQ) (s : Set X) (hfin : μ s ≠ ∞)
    (B : Euclidean n ≃L[ℝ] Euclidean n) (b : Euclidean n →L[ℝ] ℝ)
    (hchange : ∀ v, SobolevSpace.restrictLp μ hQ s (sobolevColumnMap μ hQ u' v) =
      SobolevSpace.restrictLp μ hQ s (sobolevColumnMap μ hQ u (B v)) +
        b v • restrictedOne μ s hfin) :
    affineProjection μ hQ u' s hfin = affineProjection μ hQ u s hfin := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.restrictedOne, OAI.RegularPointCoordinates.affineProjection

theorem OAI.RegularPointCoordinates.affineResidual_eq_of_change line 55