FrozenJetTransport.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite-order transport of jets through frozen affine coordinates

The input linear map and every output normalization are fixed at the testing point. Positive-order jets ignore output translations. The dyadic result therefore applies in every order used by the iteration without assuming any next-stage jet bound.

theorem OAI.RegularPointCoordinates.iteratedFDeriv_comp_clm_at line 28

Source documentation

Local finite differentiability suffices for exact linear input transport.

theorem iteratedFDeriv_comp_clm_at (L : G →L[ℝ] E) (f : E → F) (z : G) (m : ℕ)
    (hf : ContDiffAt ℝ m f (L z)) :
    iteratedFDeriv ℝ m (f ∘ L) z =
      (iteratedFDeriv ℝ m f (L z)).compContinuousLinearMap (fun _ => L) := by
…

theorem OAI.RegularPointCoordinates.iteratedFDeriv_comp_affine_at line 43

Source documentation

Exact affine input transport in every derivative order, including zero.

theorem iteratedFDeriv_comp_affine_at (L : G →L[ℝ] E) (f : E → F)
    (x : E) (z : G) (m : ℕ) (hf : ContDiffAt ℝ m f (x + L z)) :
    iteratedFDeriv ℝ m (fun y => f (x + L y)) z =
      (iteratedFDeriv ℝ m f (x + L z)).compContinuousLinearMap (fun _ => L) := by
…

theorem OAI.RegularPointCoordinates.iteratedFDeriv_comp_affine_apply line 53

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_comp_affine_le line 62

Source documentation

The norm cost of affine input transport is exactly the product of the input operator norms, with no extra combinatorial coefficient.

theorem norm_iteratedFDeriv_comp_affine_le (L : G →L[ℝ] E) (f : E → F)
    (x : E) (z : G) (m : ℕ) (hf : ContDiffAt ℝ m f (x + L z)) :
    ‖iteratedFDeriv ℝ m (fun y => f (x + L y)) z‖ ≤
      ‖iteratedFDeriv ℝ m f (x + L z)‖ * ‖L‖ ^ m := by
…

theorem OAI.RegularPointCoordinates.iteratedFDeriv_affine_input_output line 72

Source documentation

A fixed linear output map and a translation have the expected positive-order derivative.

theorem iteratedFDeriv_affine_input_output (L : G →L[ℝ] E) (A : F →L[ℝ] H)
    (f : E → F) (x : E) (z : G) (b : H) {m : ℕ} (hm : 0 < m)
    (hf : ContDiffAt ℝ m f (x + L z)) :
    iteratedFDeriv ℝ m (fun y => A (f (x + L y)) + b) z =
      A.compContinuousMultilinearMap
        ((iteratedFDeriv ℝ m f (x + L z)).compContinuousLinearMap (fun _ => L)) := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_affine_input_output_le line 89

theorem OAI.RegularPointCoordinates.iteratedFDeriv_scaled_affine line 105

Source documentation

Scalar output scaling, with arbitrary output translation.

theorem iteratedFDeriv_scaled_affine (L : G →L[ℝ] E) (f : E → F)
    (x : E) (z : G) (a : ℝ) (b : F) {m : ℕ} (hm : 0 < m)
    (hf : ContDiffAt ℝ m f (x + L z)) :
    iteratedFDeriv ℝ m (fun y => a • f (x + L y) + b) z =
      a • (iteratedFDeriv ℝ m f (x + L z)).compContinuousLinearMap (fun _ => L) := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_scaled_affine_le line 118

theorem OAI.RegularPointCoordinates.normalized_jet_apply line 132

Source documentation

The actual normalization hhat(z) = r⁻¹(h(x+r T⁻¹z)-h(x)).

theorem normalized_jet_apply (T : E ≃L[ℝ] E) (h : E → F) (x z : E) (r : ℝ)
    {m : ℕ} (hm : 0 < m) (hh : ContDiffAt ℝ m h (x + r • T.symm z))
    (xi : Fin m → E) :
    iteratedFDeriv ℝ m (fun y => r⁻¹ • (h (x + r • T.symm y) - h x)) z xi =
      (r⁻¹ * r ^ m) • iteratedFDeriv ℝ m h (x + r • T.symm z)
        (fun i => T.symm (xi i)) := by
…

theorem OAI.RegularPointCoordinates.normalized_jet_norm_le line 152

Source documentation

Operator-norm form of the same source normalization.

theorem normalized_jet_norm_le (T : E ≃L[ℝ] E) (h : E → F) (x z : E) (r : ℝ)
    {m : ℕ} (hm : 0 < m) (hh : ContDiffAt ℝ m h (x + r • T.symm z)) :
    ‖iteratedFDeriv ℝ m (fun y => r⁻¹ • (h (x + r • T.symm y) - h x)) z‖ ≤
      |r⁻¹| * ‖iteratedFDeriv ℝ m h (x + r • T.symm z)‖ *
        (|r| * ‖(T.symm : E →L[ℝ] E)‖) ^ m := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_dyadic_metric_change_le line 168

Source documentation

The dyadic change of variables for a contracting change of frozen metric. The harmless output constant is retained explicitly.

theorem norm_iteratedFDeriv_dyadic_metric_change_le (S : E →L[ℝ] E)
    (g : E → F) (b : F) {m : ℕ} (hm : 0 < m)
    (hS : ‖S‖ ≤ 1) (hg : ContDiffAt ℝ m g 0) :
    ‖iteratedFDeriv ℝ m (fun z => (2 : ℝ) • g ((1 / 2 : ℝ) • S z) + b) 0‖ ≤
      (2 / (2 : ℝ) ^ m) * ‖iteratedFDeriv ℝ m g 0‖ := by
…