NormalizedUpdate.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The coordinate update in frozen coordinates

The source coordinate and its dual covector are transformed together. Consequently the inverse-transpose update has exactly the same form in the normalized variables; no norm of the coordinate change occurs.

def OAI.RegularPointCoordinates.frozenSource line 23
Source documentation
Affine coordinates frozen at a point and a scale.
```
def frozenSource (r : ℝ) (T : E ≃L[ℝ] E) (x z : E) : E := x + r • T.symm z
```
def OAI.RegularPointCoordinates.normalizedCoordinates line 26
Source documentation
The normalized coordinate map, with its value at the center removed.
```
def normalizedCoordinates (r : ℝ) (T : E ≃L[ℝ] E) (x : E) (h : E → E)
    (z : E) : E := r⁻¹ • (h (frozenSource r T x z) - h x)
```
Mentions: OAI.RegularPointCoordinates.frozenSource
def OAI.RegularPointCoordinates.normalizedCovector line 30
Source documentation
The covector field uses the dual coordinate change.
```
def normalizedCovector (r : ℝ) (T : E ≃L[ℝ] E) (x : E) (v : E → E)
    (z : E) : E :=
…
```

theorem OAI.RegularPointCoordinates.fderiv_normalizedCoordinates line 36

Source documentation

The scale cancels out of the normalized Jacobian.

theorem fderiv_normalizedCoordinates {r : ℝ} (hr : r ≠ 0)
    (T : E ≃L[ℝ] E) (x z : E) (h : E → E)
    (hh : DifferentiableAt ℝ h (frozenSource r T x z)) :
    fderiv ℝ (normalizedCoordinates r T x h) z =
      fderiv ℝ h (frozenSource r T x z) ∘L (T.symm : E →L[ℝ] E) := by
…

Mentions: OAI.RegularPointCoordinates.frozenSource, OAI.RegularPointCoordinates.normalizedCoordinates

theorem OAI.RegularPointCoordinates.inverseTranspose_normalized_apply line 55
Source documentation
Exact covariance of the inverse transpose when the covector uses the dual change of basis.
```
theorem inverseTranspose_normalized_apply (T J : E ≃L[ℝ] E) (w : E) :
    inverseTranspose (T.symm.trans J) ((T.symm : E →L[ℝ] E).adjoint w) =
      inverseTranspose J w := by
…
```
Mentions: OAI.RegularPointCoordinates.inverseTranspose

theorem OAI.RegularPointCoordinates.normalized_update_identity line 70

Source documentation

The actual normalized update is the normalized old map plus its inverse-transpose correction. Centering at the new map only changes this expression by a constant, handled by the jet transport lemmas.

theorem normalized_update_identity {r : ℝ} (hr : r ≠ 0)
    (T : E ≃L[ℝ] E) (x z : E) (h v : E → E)
    (hh : DifferentiableAt ℝ h (frozenSource r T x z))
    (J : E ≃L[ℝ] E)
    (hJ : fderiv ℝ h (frozenSource r T x z) = (J : E →L[ℝ] E)) :
    r⁻¹ • (h (frozenSource r T x z) +
        operatorInverseTranspose (fderiv ℝ h (frozenSource r T x z))
          (v (frozenSource r T x z)) - h x) =
      normalizedCoordinates r T x h z +
        operatorInverseTranspose (fderiv ℝ (normalizedCoordinates r T x h) z)
          (normalizedCovector r T x v z) := by
…

Mentions: OAI.RegularPointCoordinates.frozenSource, OAI.RegularPointCoordinates.operatorInverseTranspose, OAI.RegularPointCoordinates.normalizedCoordinates, OAI.RegularPointCoordinates.normalizedCovector