InverseDerivative.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Inverse-transpose differentiation and contraction

The metric iteration uses cancellation before estimating the derivative of an inverse transpose. These identities work with bounded operators on any real Hilbert space; no matrix coordinates or condition-number bounds enter the cancellation itself.

def OAI.RegularPointCoordinates.inverseTranspose line 28
Source documentation
The adjoint of the inverse of a bounded linear equivalence.
```
def inverseTranspose (J : E ≃L[ℝ] E) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.inner_apply_inverseTranspose line 32
Source documentation
The inverse transpose cancels the undifferentiated Jacobian in an inner product.
```
theorem inner_apply_inverseTranspose (J : E ≃L[ℝ] E) (ξ w : E) :
    ⟪J ξ, inverseTranspose J w⟫_ℝ = ⟪ξ, w⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.inverseTranspose
def OAI.RegularPointCoordinates.inverseTransposeVariation line 38
Source documentation
The first variation of an inverse transpose.
```
def inverseTransposeVariation (J : E ≃L[ℝ] E) (dJ : E →L[ℝ] E) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.inner_apply_inverseTransposeVariation line 43
Source documentation
Exact cancellation in the differentiated inverse-transpose term. This is the operator form of re:inverse-transpose-contraction.
```
theorem inner_apply_inverseTransposeVariation (J : E ≃L[ℝ] E)
    (dJ : E →L[ℝ] E) (ξ w : E) :
    ⟪J ξ, inverseTransposeVariation J dJ w⟫_ℝ =
      -⟪dJ ξ, inverseTranspose J w⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.inverseTransposeVariation, OAI.RegularPointCoordinates.inverseTranspose
theorem OAI.RegularPointCoordinates.abs_inner_apply_inverseTransposeVariation_le line 52
Source documentation
The differentiated-inverse error is controlled by the diagonal Jacobian derivative, with no operator norm of that derivative.
```
theorem abs_inner_apply_inverseTransposeVariation_le (J : E ≃L[ℝ] E)
    (dJ : E →L[ℝ] E) (ξ w : E) :
    |⟪J ξ, inverseTransposeVariation J dJ w⟫_ℝ| ≤
      ‖dJ ξ‖ * ‖inverseTranspose J w‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.inverseTransposeVariation, OAI.RegularPointCoordinates.inverseTranspose

theorem OAI.RegularPointCoordinates.norm_sq_inverseTranspose_increment line 61

Source documentation

The exact metric increment splits into the principal term, the diagonal differentiated-inverse error, and the squared increment.

theorem norm_sq_inverseTranspose_increment (J : E ≃L[ℝ] E)
    (dJ : E →L[ℝ] E) (ξ dv v : E) :
    ‖J ξ + (inverseTranspose J dv + inverseTransposeVariation J dJ v)‖ ^ 2 -
        ‖J ξ‖ ^ 2 =
      2 * ⟪ξ, dv⟫_ℝ - 2 * ⟪dJ ξ, inverseTranspose J v⟫_ℝ +
        ‖inverseTranspose J dv + inverseTransposeVariation J dJ v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.inverseTranspose, OAI.RegularPointCoordinates.inverseTransposeVariation

theorem OAI.RegularPointCoordinates.hasFDerivAt_operator_inverse line 72

Source documentation

Fréchet derivative of inversion at a bounded linear equivalence.

theorem hasFDerivAt_operator_inverse (J : E ≃L[ℝ] E) :
    HasFDerivAt (Ring.inverse : (E →L[ℝ] E) → E →L[ℝ] E)
      (-mulLeftRight ℝ (E →L[ℝ] E) (J.symm : E →L[ℝ] E)
        (J.symm : E →L[ℝ] E)) (J : E →L[ℝ] E) := by
…

def OAI.RegularPointCoordinates.adjointOperator line 79
Source documentation
The adjoint operation, viewed as a real continuous linear map.
```
def adjointOperator : (E →L[ℝ] E) →L[ℝ] (E →L[ℝ] E) :=
…
```
def OAI.RegularPointCoordinates.operatorInverseTranspose line 84
Source documentation
The inverse-transpose operation on all bounded operators. Only its behavior at an invertible operator is used.
```
def operatorInverseTranspose (J : E →L[ℝ] E) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.operatorInverseTranspose_equiv line 87

theorem OAI.RegularPointCoordinates.hasFDerivAt_operator_inverseTranspose line 94

Source documentation

Differentiating the inverse transpose of a varying Jacobian.

theorem hasFDerivAt_operator_inverseTranspose (J : E ≃L[ℝ] E) :
    HasFDerivAt (operatorInverseTranspose : (E →L[ℝ] E) → E →L[ℝ] E)
      (adjointOperator ∘L
        (-mulLeftRight ℝ (E →L[ℝ] E) (J.symm : E →L[ℝ] E)
          (J.symm : E →L[ℝ] E))) (J : E →L[ℝ] E) := by
…

Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose, OAI.RegularPointCoordinates.adjointOperator

theorem OAI.RegularPointCoordinates.inverseTranspose_derivative_apply line 102
Source documentation
The derivative above is exactly the inverse-transpose variation.
```
theorem inverseTranspose_derivative_apply (J : E ≃L[ℝ] E) (dJ : E →L[ℝ] E) :
    (adjointOperator ∘L
      (-mulLeftRight ℝ (E →L[ℝ] E) (J.symm : E →L[ℝ] E)
        (J.symm : E →L[ℝ] E))) dJ = inverseTransposeVariation J dJ := by
…
```
Mentions: OAI.RegularPointCoordinates.adjointOperator, OAI.RegularPointCoordinates.inverseTransposeVariation

theorem OAI.RegularPointCoordinates.inverseTranspose_fderiv_contraction line 111

Source documentation

The cancellation for the actual directional Fréchet derivative of a variable inverse transpose.

theorem inverseTranspose_fderiv_contraction
    {J : X → E →L[ℝ] E} {J' : X →L[ℝ] (E →L[ℝ] E)} {x : X}
    (e : E ≃L[ℝ] E) (he : J x = (e : E →L[ℝ] E))
    (hJ : HasFDerivAt J J' x) (u : X) (ξ w : E) :
    ⟪e ξ, (fderiv ℝ (fun y => operatorInverseTranspose (J y)) x u) w⟫_ℝ =
      -⟪J' u ξ, inverseTranspose e w⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose, OAI.RegularPointCoordinates.inverseTranspose

theorem OAI.RegularPointCoordinates.abs_inverseTranspose_fderiv_contraction_le line 125

Source documentation

The same diagonal bound for the actual directional derivative.

theorem abs_inverseTranspose_fderiv_contraction_le
    {J : X → E →L[ℝ] E} {J' : X →L[ℝ] (E →L[ℝ] E)} {x : X}
    (e : E ≃L[ℝ] E) (he : J x = (e : E →L[ℝ] E))
    (hJ : HasFDerivAt J J' x) (u : X) (ξ w : E) :
    |⟪e ξ, (fderiv ℝ (fun y => operatorInverseTranspose (J y)) x u) w⟫_ℝ| ≤
      ‖J' u ξ‖ * ‖inverseTranspose e w‖ := by
…

Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose, OAI.RegularPointCoordinates.inverseTranspose