Source indexedlemma · leanprover/lean4:v4.32.0

lower_secant_bound

Carleson.Classical.Basic · Carleson/Classical/Basic.lean:306 to 321

Mathematical statement

Exact Lean statement

lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π + η) (2 * π - η)) (xAbs : η ≤ |x|) :
    η / 2 ≤ ‖(1 - Complex.exp (Complex.I * x))‖

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π + η) (2 * π - η)) (xAbs : η ≤ |x|) :    η / 2 ≤ ‖(1 - Complex.exp (Complex.I * x))‖ := by  by_cases! ηpos : η < 0  · calc η / 2    _ ≤ 0 := by linarith    _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := norm_nonneg _  calc η / 2  _ ≤ (2 / π) * η := by    ring_nf    rw [mul_assoc]    gcongr    field_simp    norm_num [pi_le_four]  _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by    apply lower_secant_bound' xAbs    rwa [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]