DifferentialStep.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Differential identities for the metric iteration

These identities concern the actual update h + (Dh)⁻ᵀ v. In particular, the second derivative includes both mixed terms and the second derivative of the inverse field. The metric identity keeps the diagonal cancellation before taking norms.

def OAI.RegularPointCoordinates.diagonalSecond line 29
Source documentation
The second derivative in one direction, expressed without choosing coordinates on the space of bilinear maps.
```
def diagonalSecond (f : E → F) (x ξ : E) : F :=
…
```

theorem OAI.RegularPointCoordinates.fderiv_apply_fixed line 34

Source documentation

Evaluating the derivative of a linear-map-valued function commutes with evaluation on a fixed vector.

theorem fderiv_apply_fixed {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    {A : E → F →L[ℝ] G} {x : E} (hA : DifferentiableAt ℝ A x) (u : E)
    (v : F) :
    fderiv ℝ (fun y => A y v) x u = fderiv ℝ A x u v := by
…

theorem OAI.RegularPointCoordinates.diagonalSecond_eq line 43
Source documentation
The directional form is the diagonal evaluation of the genuine second Fréchet derivative.
```
theorem diagonalSecond_eq {f : E → F} {x : E}
    (hf : ContDiffAt ℝ 2 f x) (ξ : E) :
    diagonalSecond f x ξ = iteratedFDeriv ℝ 2 f x (fun _ => ξ) := by
…
```
Mentions: OAI.RegularPointCoordinates.diagonalSecond

theorem OAI.RegularPointCoordinates.diagonalSecond_clm_apply line 52

Source documentation

All three terms of the second derivative of an operator applied to a vector field, with the two equal mixed terms combined.

theorem diagonalSecond_clm_apply {K : E → F →L[ℝ] F} {v : E → F} {x : E}
    (hK : ContDiffAt ℝ 2 K x) (hv : ContDiffAt ℝ 2 v x) (ξ : E) :
    diagonalSecond (fun y => K y (v y)) x ξ =
      K x (diagonalSecond v x ξ) +
        2 • (fderiv ℝ K x ξ (fderiv ℝ v x ξ)) +
        diagonalSecond K x ξ (v x) := by
…

Mentions: OAI.RegularPointCoordinates.diagonalSecond

theorem OAI.RegularPointCoordinates.diagonalSecond_add line 84

Source documentation

Addition of maps preserves the actual second directional derivative.

theorem diagonalSecond_add {f g : E → F} {x : E}
    (hf : ContDiffAt ℝ 2 f x) (hg : ContDiffAt ℝ 2 g x) (ξ : E) :
    diagonalSecond (fun y => f y + g y) x ξ =
      diagonalSecond f x ξ + diagonalSecond g x ξ := by
…

Mentions: OAI.RegularPointCoordinates.diagonalSecond

theorem OAI.RegularPointCoordinates.inverseTranspose_update_metric_increment line 99
Source documentation
The exact metric increment for the genuine update. The derivative of the inverse transpose is contracted with the old Jacobian before being estimated, so only the diagonal second derivative of h remains.
```
theorem inverseTranspose_update_metric_increment
    {h v : E → E} {x : E} (hh : ContDiffAt ℝ 2 h x)
    (hv : DifferentiableAt ℝ v x) (J : E ≃L[ℝ] E)
    (hJ : fderiv ℝ h x = (J : E →L[ℝ] E)) (ξ : E) :
    let next := fun y => h y + operatorInverseTranspose (fderiv ℝ h y) (v y)
…
```
Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose

theorem OAI.RegularPointCoordinates.exists_inverseTranspose_low_order_cost line 139

Source documentation

The first two inverse-field costs follow from only three source derivatives. The same constant works for every point and jet base.

theorem exists_inverseTranspose_low_order_cost {A : ℝ} (hA : 1 ≤ A) :
    ∃ C : ℝ, Real.sqrt A ≤ C ∧ 2 * A ≤ C ∧
      ∀ (B : ℝ), 0 < B → ∀ (h : E → E) (x : E),
      ContDiffAt ℝ 3 h x → IsUnit (fderiv ℝ h x) →
      ‖Ring.inverse (fderiv ℝ h x)‖ ≤ Real.sqrt A →
      (∀ m, 2 ≤ m → m ≤ 3 → ‖iteratedFDeriv ℝ m h x‖ ≤
        B ^ (m - 1) * (m.factorial : ℝ) ^ 3) →
      let K := fun y => operatorInverseTranspose (fderiv ℝ h y)
…

Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose