TaylorControl.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Taylor control on a coordinate-value segment

The final pair estimate only differentiates maps in Euclidean coordinate value space. This lemma isolates that calculation, with an explicit second derivative and no differentiability assumption on the underlying metric. The bound has constant one; the final scale can absorb this harmless choice.

theorem OAI.RegularPointCoordinates.norm_unit_interval_taylor_remainder_le line 23

Source documentation

First-order Taylor control along a unit parameter interval.

theorem norm_unit_interval_taylor_remainder_le
    {f g k : ℝ → F} {M : ℝ} (hM : 0 ≤ M)
    (hf : ∀ t ∈ Icc (0 : ℝ) 1, HasDerivAt f (g t) t)
    (hg : ∀ t ∈ Icc (0 : ℝ) 1, HasDerivAt g (k t) t)
    (hk : ∀ t ∈ Icc (0 : ℝ) 1, ‖k t‖ ≤ M) :
    ‖f 1 - f 0 - g 0‖ ≤ M := by
…

theorem OAI.RegularPointCoordinates.norm_taylor_remainder_le_directional line 44

Source documentation

Only the second derivative in the direction of the segment is needed. This form allows an arbitrary anisotropic frozen metric in the application.

theorem norm_taylor_remainder_le_directional
    {f : E → F} {df : E → E →L[ℝ] F}
    {ddf : E → E →L[ℝ] (E →L[ℝ] F)} {x z : E} {M : ℝ}
    (hM : 0 ≤ M)
    (hf : ∀ y ∈ segment ℝ x z, HasFDerivAt f (df y) y)
    (hdf : ∀ y ∈ segment ℝ x z, HasFDerivAt df (ddf y) y)
    (hbound : ∀ y ∈ segment ℝ x z, ‖ddf y (z - x) (z - x)‖ ≤ M) :
    ‖f z - f x - df x (z - x)‖ ≤ M := by
…

theorem OAI.RegularPointCoordinates.norm_taylor_remainder_le line 73

Source documentation

A bound on the second derivative gives a quadratic Taylor error along one segment. No convexity beyond that single segment is required.

theorem norm_taylor_remainder_le
    {f : E → F} {df : E → E →L[ℝ] F}
    {ddf : E → E →L[ℝ] (E →L[ℝ] F)} {x z : E} {M : ℝ}
    (hM : 0 ≤ M)
    (hf : ∀ y ∈ segment ℝ x z, HasFDerivAt f (df y) y)
    (hdf : ∀ y ∈ segment ℝ x z, HasFDerivAt df (ddf y) y)
    (hbound : ∀ y ∈ segment ℝ x z, ‖ddf y‖ ≤ M) :
    ‖f z - f x - df x (z - x)‖ ≤ M * ‖z - x‖ ^ 2 := by
…

theorem OAI.RegularPointCoordinates.dist_bounds_of_taylor line 97

Source documentation

Taylor control combined with bounds on the linearized image.

theorem dist_bounds_of_taylor
    {f : E → F} {df : E → E →L[ℝ] F}
    {ddf : E → E →L[ℝ] (E →L[ℝ] F)} {x z : E}
    {M a b t e : ℝ} (hM : 0 ≤ M)
    (hf : ∀ y ∈ segment ℝ x z, HasFDerivAt f (df y) y)
    (hdf : ∀ y ∈ segment ℝ x z, HasFDerivAt df (ddf y) y)
    (hbound : ∀ y ∈ segment ℝ x z, ‖ddf y‖ ≤ M)
    (hlower : a * t ≤ ‖df x (z - x)‖)
    (hupper : ‖df x (z - x)‖ ≤ b * t)
    (hsmall : M * ‖z - x‖ ^ 2 ≤ e * t) :
    (a - e) * t ≤ dist (f z) (f x) ∧ dist (f z) (f x) ≤ (b + e) * t := by
…

theorem OAI.RegularPointCoordinates.dist_bounds_of_directional_taylor line 116

Source documentation

The metric comparison using only the diagonal second derivative.

theorem dist_bounds_of_directional_taylor
    {f : E → F} {df : E → E →L[ℝ] F}
    {ddf : E → E →L[ℝ] (E →L[ℝ] F)} {x z : E}
    {M a b t e : ℝ} (hM : 0 ≤ M)
    (hf : ∀ y ∈ segment ℝ x z, HasFDerivAt f (df y) y)
    (hdf : ∀ y ∈ segment ℝ x z, HasFDerivAt df (ddf y) y)
    (hbound : ∀ y ∈ segment ℝ x z, ‖ddf y (z - x) (z - x)‖ ≤ M)
    (hlower : a * t ≤ ‖df x (z - x)‖)
    (hupper : ‖df x (z - x)‖ ≤ b * t)
    (hsmall : M ≤ e * t) :
    (a - e) * t ≤ dist (f z) (f x) ∧ dist (f z) (f x) ≤ (b + e) * t := by
…