RadialCoefficientMatrix.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Stacking the scalar radial fits in the same normalizing frame

def OAI.RegularPointCoordinates.radialCoefficientMatrix line 12
theorem OAI.RegularPointCoordinates.radialCoefficientMatrix_action line 18
Source documentation
The stacked coefficient matrix acts on normalized coordinate values by the original scalar affine coefficients.
```
theorem radialCoefficientMatrix_action {n : ℕ}
    (N : Euclidean n ≃L[ℝ] Euclidean n) (coeff : Fin n → Euclidean n)
    (x : Euclidean n) (i : Fin n) :
    Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℝ) (radialCoefficientMatrix N coeff)
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.radialCoefficientMatrix

theorem OAI.RegularPointCoordinates.radialCoefficientMatrix_sub_id_norm line 33

Source documentation

The scalar coefficient errors give a near-identity matrix in the operator norm, with only the fixed dimension loss.

theorem radialCoefficientMatrix_sub_id_norm {n : ℕ}
    (N : Euclidean n ≃L[ℝ] Euclidean n) (coeff : Fin n → Euclidean n)
    {η : ℝ} (hη : 0 ≤ η)
    (hcoeff : ∀ i, ‖N.symm (coeff i - N (EuclideanSpace.single i 1))‖ ≤ η) :
    ‖Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℝ) (radialCoefficientMatrix N coeff) -
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.radialCoefficientMatrix