`BookProof.ChapterResidualStream.norm_residual_sub_le` {f : E → E} {L : ℝ} (hf : ∀ x y, ‖f x - f y‖ ≤ L * ‖x - y‖) (x y : E) : ‖residual f x - residual f y‖ ≤ (1 + L) * ‖x...
ProvedBookProof.ChapterResidualStream.norm_residual_sub_letheoremstimepiece
Prove the following Lean 4 theorem from ChapterResidualStream.
BookProof.ChapterResidualStream.norm_residual_sub_le {f : E → E} {L : ℝ} (hf : ∀ x y, ‖f x - f y‖ ≤ L * ‖x - y‖) (x y : E) : ‖residual f x - residual f y‖ ≤ (1 + L) * ‖x - y‖
Formalization note: Lean 4 identifier BookProof.ChapterResidualStream.norm_residual_sub_le.
Preamble
-- Generated from ChapterResidualStream.lean — theorem BookProof.ChapterResidualStream.norm_residual_sub_le
import Definitions.Def_ChapterSoftmaxSharpness
import Definitions.Def_ChapterAttentionOutput
import Mathlib
import Definitions.Def_ChapterResidualStream
open BookProof.ChapterResidualStream
open scoped BigOperators
noncomputable section
open BookProof.ChapterSoftmaxSharpness BookProof.ChapterAttentionOutput
variable {m : ℕ} {E : Type*} [NormedAddCommGroup E]Formal statement
theorem BookProof.ChapterResidualStream.norm_residual_sub_le {f : E → E} {L : ℝ}
(hf : ∀ x y, ‖f x - f y‖ ≤ L * ‖x - y‖) (x y : E) :
‖residual f x - residual f y‖ ≤ (1 + L) * ‖x - y‖ := by sorry