RebasedRadialFits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Rewriting the actual radial affine fits in one centered frame

def OAI.RegularPointCoordinates.rebasedRadialOperator line 15
Source documentation
The covector coefficient of a radial fit after changing its input frame from M to N.
```
def rebasedRadialOperator {n : ℕ} (N M : Euclidean n ≃L[ℝ] Euclidean n)
    (C : Euclidean n →L[ℝ] Euclidean n) : Euclidean n →L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.rebased_radial_operator_bound line 21

Source documentation

The two frame factors are the only loss in the near-identity estimate.

theorem rebased_radial_operator_bound {n : ℕ}
    (N M : Euclidean n ≃L[ℝ] Euclidean n) (C : Euclidean n →L[ℝ] Euclidean n) :
    ‖rebasedRadialOperator N M C - 1‖ ≤
      ‖N.symm.toContinuousLinearMap.comp M.toContinuousLinearMap‖ *
      ‖M.symm.toContinuousLinearMap.comp C - 1‖ *
      ‖M.symm.toContinuousLinearMap.comp N.toContinuousLinearMap‖ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.rebasedRadialOperator

theorem OAI.RegularPointCoordinates.rebased_radial_operator_bound_two line 40

Source documentation

The nearby exact frames lose at most a factor two in the actual radial operator's near-identity error.

theorem rebased_radial_operator_bound_two {n : ℕ}
    (N M : Euclidean n ≃L[ℝ] Euclidean n) (C : Euclidean n →L[ℝ] Euclidean n)
    {δ : ℝ}
    (hN : ‖N.symm.toContinuousLinearMap.comp M.toContinuousLinearMap‖ ≤ Real.sqrt 2)
    (hM : ‖M.symm.toContinuousLinearMap.comp N.toContinuousLinearMap‖ ≤ Real.sqrt 2)
    (hC : ‖M.symm.toContinuousLinearMap.comp C - 1‖ ≤ δ) :
    ‖rebasedRadialOperator N M C - 1‖ ≤ 2 * δ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.rebasedRadialOperator

theorem OAI.RegularPointCoordinates.centered_radial_rebase line 61

Source documentation

Recentering adds exactly the constant determined by the displacement of the centers. No gradient or value error is introduced by this rewrite.

theorem centered_radial_rebase {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (η : SobolevSpace μ hQ)
    (x z : Euclidean n) (N M : Euclidean n ≃L[ℝ] Euclidean n)
    (C : Euclidean n →L[ℝ] Euclidean n) (b : Euclidean n) :
    centeredAffineSobolev μ hQ u η x (C (M.symm (N b))) =
      (centeredSobolevMap μ hQ u η z).comp N.toContinuousLinearMap
        (rebasedRadialOperator N M C b) +
      ⟪z - x, C (M.symm (N b))⟫_ℝ • η := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.centeredAffineSobolev, OAI.RegularPointCoordinates.centeredSobolevMap, OAI.RegularPointCoordinates.rebasedRadialOperator