Inner products along a linear approximation #
If a vector y' follows the linear expansion y + A (z - x) up to ε * ‖z - x‖, and z lies on
the segment x + t • h, then pairing with h gives ⟪h, y'⟫ = ⟪h, y⟫ + t * ⟪h, A h⟫ up to
ε * ‖h‖ ^ 2.
Main results #
TauCeti.abs_inner_sub_inner_sub_mul_le: the bound on the pairing withh.
theorem
TauCeti.abs_inner_sub_inner_sub_mul_le
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{z x y y' h : E}
{A : E →ₗ[ℝ] E}
{t ε : ℝ}
(hε : 0 ≤ ε)
(hz : z - x = t • h)
(hzh : ‖z - x‖ ≤ ‖h‖)
(hb : ‖y' - y - A (z - x)‖ ≤ ε * ‖z - x‖)
:
Along the segment x + t • h, a vector y' which follows the expansion
y + A (z - x) up to ε * ‖z - x‖ satisfies ⟪h, y'⟫ = ⟪h, y⟫ + t * ⟪h, A h⟫ up to
ε * ‖h‖ ^ 2.