FrozenInverseCosts.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Inverse-derivative costs in frozen coordinates

The covariance identity is used only near the testing point, where the Jacobian is represented by continuous linear equivalences. Differentiating this local identity transports the normalized inverse costs with exactly one factor of r⁻¹ per source derivative.

theorem OAI.RegularPointCoordinates.iteratedFDeriv_clm_apply_fixed line 26

Source documentation

Evaluation on a fixed vector commutes with each finite-order derivative.

theorem iteratedFDeriv_clm_apply_fixed {K : E → E →L[ℝ] E} {x : E} {m : ℕ}
    (hK : ContDiffAt ℝ m K x) (w : E) (xi : Fin m → E) :
    iteratedFDeriv ℝ m (fun y => K y w) x xi = iteratedFDeriv ℝ m K x xi w := by
…

theorem OAI.RegularPointCoordinates.frozen_operator_jet_transport line 33

Source documentation

Transport of operator jets through a local frozen covariance identity.

theorem frozen_operator_jet_transport (T : E ≃L[ℝ] E) (x xi w : E) (r : ℝ)
    {Ko Kn : E → E →L[ℝ] E} {m : ℕ}
    (hKo : ContDiffAt ℝ m Ko x) (hKn : ContDiffAt ℝ m Kn 0)
    (hcov : (fun z => Kn z ((T.symm : E →L[ℝ] E).adjoint w)) =ᶠ[𝓝 0]
      (fun z => Ko (frozenSource r T x z) w)) :
    iteratedFDeriv ℝ m Kn 0 (fun _ => T xi) ((T.symm : E →L[ℝ] E).adjoint w) =
      r ^ m • iteratedFDeriv ℝ m Ko x (fun _ => xi) w := by
…

Mentions: OAI.RegularPointCoordinates.frozenSource

theorem OAI.RegularPointCoordinates.inverseTranspose_normalized_eventually line 59

Source documentation

The inverse covariance holds in a neighborhood, so it may be differentiated without assuming invertibility away from that neighborhood.

theorem inverseTranspose_normalized_eventually {r : ℝ} (hr : r ≠ 0)
    (T : E ≃L[ℝ] E) (x : E) (h : E → E) (e : E → E ≃L[ℝ] E)
    (hh : ContDiffAt ℝ 3 h x)
    (hlocal : ∀ᶠ y in 𝓝 x, fderiv ℝ h y = (e y : E →L[ℝ] E)) (w : E) :
    (fun z => operatorInverseTranspose (fderiv ℝ (normalizedCoordinates r T x h) z)
      ((T.symm : E →L[ℝ] E).adjoint w)) =ᶠ[𝓝 0]
    (fun z => operatorInverseTranspose (fderiv ℝ h (frozenSource r T x z)) w) := by
…

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

theorem OAI.RegularPointCoordinates.exists_frozen_inverse_derivative_cost line 83

Source documentation

The lower metric estimate and normalized source jets imply the first two original-space inverse costs, with the same constant at every point and scale. All invertibility data outside the center are local.

theorem exists_frozen_inverse_derivative_cost {A : ℝ} (hA : 1 ≤ A) :
    ∃ C : ℝ, Real.sqrt A ≤ C ∧ 2 * A ≤ C ∧
      ∀ (B r : ℝ), 0 < B → 0 < r → ∀ (T : E ≃L[ℝ] E) (x : E)
        (h : E → E) (e : E → E ≃L[ℝ] E),
      ContDiffAt ℝ 3 h x →
      (∀ᶠ y in 𝓝 x, fderiv ℝ h y = (e y : E →L[ℝ] E)) →
      (∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖fderiv ℝ h x xi‖ ^ 2) →
      (∀ m, 2 ≤ m → m ≤ 3 →
        ‖iteratedFDeriv ℝ m (normalizedCoordinates r T x h) 0‖ ≤
          B ^ (m - 1) * (m.factorial : ℝ) ^ 3) →
      let K := fun y => operatorInverseTranspose (fderiv ℝ h y)
…

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