OAI/Geometry/RCD/Coordinates/NormalizedJetStep.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The normalized coordinate update

The update is h + (Dh)⁻ᵀ v. Inverse-transpose bounds, the bilinear product estimate, and scalar dyadic contraction control iterated Fréchet derivatives with one positive parameter for every order.

  1. theorem OAI.RegularPointCoordinates.clm_apply_factorialMajorant_bound_at line 28

    Source documentation

    The factorial product bound also holds for smoothness only at the base point. Each finite order uses a common open neighborhood.

    theorem clm_apply_factorialMajorant_bound_at
    {f : X → F →L[ℝ] G} {g : X → F} {x : X}
    {B C D : ℝ} {m : ℕ} (hB : 0 < B) (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hf : ContDiffAt ℝ m f x) (hg : ContDiffAt ℝ m g x)
    (hfbound : ∀ i, i ≤ m → ‖iteratedFDeriv ℝ i f x‖ ≤
      C * factorialMajorant i * jetCoefficientScale B i)
    (hgbound : ∀ i, i ≤ m → ‖iteratedFDeriv ℝ i g x‖ ≤
      D * factorialMajorant i * jetCoefficientScale B i) :
    ‖iteratedFDeriv ℝ m (fun y => f y (g y)) x‖ ≤
      (10 * C * D) * factorialMajorant m * jetCoefficientScale B m := by
…

    Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

  2. theorem OAI.RegularPointCoordinates.contDiffAt_inverseTranspose_field line 56

    Source documentation

    Smoothness of the inverse-transpose field is automatic at each point at which the Jacobian is invertible.

    theorem contDiffAt_inverseTranspose_field
    {J : X → E →L[ℝ] E} {x : X} {m : ℕ}
    (hJ : ContDiffAt ℝ m J x) (hunit : IsUnit (J x)) :
    ContDiffAt ℝ m (fun y => operatorInverseTranspose (J y)) x := by
…

    Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose

  3. theorem OAI.RegularPointCoordinates.jacobian_jet_bound_of_source_jet_bound line 68

    Source documentation

    The source jet bound supplies precisely the Jacobian weight used by the inverse-majorant theorem, with no enlargement of the base.

    theorem jacobian_jet_bound_of_source_jet_bound
    {h : E → E} {x : E} {B : ℝ}
    (hbound : ∀ m, 2 ≤ m → ‖iteratedFDeriv ℝ m h x‖ ≤
      B ^ (m - 1) * (m.factorial : ℝ) ^ 3)
    {m : ℕ} (hm : 0 < m) :
    ‖iteratedFDeriv ℝ m (fderiv ℝ h) x‖ ≤
      factorialMajorant m * jetCoefficientScale B m := by
…

    Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

  4. theorem OAI.RegularPointCoordinates.exists_normalized_jet_step_of_jacobian_bounds line 87

    Source documentation

    With explicit Jacobian jets, the actual inverse-transpose update preserves every normalized jet of order at least two.

    theorem exists_normalized_jet_step_of_jacobian_bounds
    {A B Cv : ℝ} (hA : 1 ≤ A) (hB : 0 < B) (hCv : 0 ≤ Cv) :
    ∃ epsilon : ℝ, 0 < epsilon ∧
      ∀ (h : E → E) (J : E → E →L[ℝ] E) (v : E → E) (x : E),
      (∀ m : ℕ, ContDiffAt ℝ m h x) →
      (∀ m : ℕ, ContDiffAt ℝ m J x) →
      (∀ m : ℕ, ContDiffAt ℝ m v x) → IsUnit (J x) →
      ‖Ring.inverse (J x)‖ ≤ Real.sqrt A →
      (∀ m, 2 ≤ m → ‖iteratedFDeriv ℝ m h x‖ ≤
        B ^ (m - 1) * (m.factorial : ℝ) ^ 3) →
      (∀ m, 0 < m → ‖iteratedFDeriv ℝ m J x‖ ≤
        factorialMajorant m * jetCoefficientScale B m) →
…

    Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

  5. theorem OAI.RegularPointCoordinates.exists_normalized_jet_step line 140

    Source documentation

    The normalized coordinate update with the genuine derivative field. There is one positive epsilon for all orders, all maps, and all base points satisfying the stated source and correction jet bounds.

    theorem exists_normalized_jet_step
    {A B Cv : ℝ} (hA : 1 ≤ A) (hB : 0 < B) (hCv : 0 ≤ Cv) :
    ∃ epsilon : ℝ, 0 < epsilon ∧
      ∀ (h v : E → E) (x : E),
      (∀ m : ℕ, ContDiffAt ℝ m h x) →
      (∀ m : ℕ, ContDiffAt ℝ m v x) → IsUnit (fderiv ℝ h x) →
      ‖Ring.inverse (fderiv ℝ h x)‖ ≤ Real.sqrt A →
      (∀ m, 2 ≤ m → ‖iteratedFDeriv ℝ m h x‖ ≤
        B ^ (m - 1) * (m.factorial : ℝ) ^ 3) →
      (∀ m, ‖iteratedFDeriv ℝ m v x‖ ≤
        epsilon * Cv * factorialMajorant m * jetCoefficientScale B m) →
      ∀ m, 2 ≤ m →
…

    Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

  6. theorem OAI.RegularPointCoordinates.inverse_jet_finite_uniform_bound line 167

    Source documentation

    The universal inverse constant also controls every finite prefix. Zero extension beyond the requested order supplies an admissible full recurrence; it does not assume any derivative bound at higher orders.

    theorem inverse_jet_finite_uniform_bound {A : ℝ} (hA : 1 ≤ A) :
    ∃ C : ℝ, Real.sqrt A ≤ C ∧ 2 * A ≤ C ∧
      ∀ (B : ℝ), 0 < B → ∀ (N : ℕ) (j k : ℕ → ℝ),
      (∀ q ≤ N, 0 ≤ j q) → (∀ q ≤ N, 0 ≤ k q) → k 0 ≤ Real.sqrt A →
      (∀ q, 0 < q → q ≤ N → j q ≤ factorialMajorant q * jetCoefficientScale B q) →
      (∀ q, 0 < q → q ≤ N → k q ≤ Real.sqrt A *
        ∑ i ∈ Finset.Icc 1 q, (q.choose i : ℝ) * j i * k (q - i)) →
      ∀ q ≤ N, k q ≤ C * factorialMajorant q * jetCoefficientScale B q := by
…

    Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

  7. theorem OAI.RegularPointCoordinates.inverseTranspose_iteratedFDeriv_finite_uniform_bound line 221

    Source documentation

    Actual inverse-transpose derivatives through a finite order use only Jacobian derivatives through that same order. The constant does not depend on the finite cutoff.

    theorem inverseTranspose_iteratedFDeriv_finite_uniform_bound {A : ℝ} (hA : 1 ≤ A) :
    ∃ C : ℝ, Real.sqrt A ≤ C ∧ 2 * A ≤ C ∧
      ∀ (B : ℝ), 0 < B → ∀ (N : ℕ) (J : E → E →L[ℝ] E) (x : E),
      ContDiffAt ℝ N J x → IsUnit (J x) → ‖Ring.inverse (J x)‖ ≤ Real.sqrt A →
      (∀ q, 0 < q → q ≤ N → ‖iteratedFDeriv ℝ q J x‖ ≤
        factorialMajorant q * jetCoefficientScale B q) →
      ∀ q ≤ N, ‖iteratedFDeriv ℝ q (fun y => operatorInverseTranspose (J y)) x‖ ≤
        C * factorialMajorant q * jetCoefficientScale B q := by
…

    Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale, OAI.RegularPointCoordinates.operatorInverseTranspose

  8. theorem OAI.RegularPointCoordinates.exists_normalized_jet_step_finite line 251

    Source documentation

    Finite-order form of the genuine coordinate update. To preserve order m, only source jets through m + 1 and correction jets through m are needed. The positive parameter is independent of m.

    theorem exists_normalized_jet_step_finite
    {A B Cv : ℝ} (hA : 1 ≤ A) (hB : 0 < B) (hCv : 0 ≤ Cv) :
    ∃ epsilon : ℝ, 0 < epsilon ∧
      ∀ (m : ℕ), 2 ≤ m → ∀ (h v : E → E) (x : E),
      ContDiffAt ℝ (m + 1) h x → ContDiffAt ℝ m v x →
      IsUnit (fderiv ℝ h x) → ‖Ring.inverse (fderiv ℝ h x)‖ ≤ Real.sqrt A →
      (∀ q, 2 ≤ q → q ≤ m + 1 → ‖iteratedFDeriv ℝ q h x‖ ≤
        B ^ (q - 1) * (q.factorial : ℝ) ^ 3) →
      (∀ q, q ≤ m → ‖iteratedFDeriv ℝ q v x‖ ≤
        epsilon * Cv * factorialMajorant q * jetCoefficientScale B q) →
      (2 / (2 : ℝ) ^ m) *
        ‖iteratedFDeriv ℝ m (fun y => h y +
…

    Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale