def
definition
def or abbrev
V_RS_quartic
show as:
view Lean formalization →
formal statement (Lean)
91def V_RS_quartic (Λ v h : ℝ) : ℝ :=
proof body
Definition body.
92 Λ ^ 4 * ((h / v) ^ 2 / 2 + (h / v) ^ 4 / 24)
93
94/-- Mathlib truncation lemma, restated for real `t` to depth 6.
95
96 `|exp t − (1 + t + t²/2 + t³/6 + t⁴/24 + t⁵/120)| ≤ exp |t| · |t|⁶`.
97
98 Proof: lift to ℂ and apply `Complex.norm_exp_sub_sum_le_norm_mul_exp`. -/