internlm/Lean-Github huggingface dataset:
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
wlog x_le_pi : x ≤ Real.pi generalizing x
Proof state after:
case inr
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
case inr
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
. convert (@this (2 * Real.pi - x) _ _ _ _) using 1
  . rw [Complex.norm_eq_abs, ←Complex.abs_conj]
    simp
    rw [←Complex.exp_conj]
    simp
    rw [mul_sub, Complex.conj_ofReal, Complex.exp_sub, mul_comm Complex.I (2 * Real.pi), Complex.exp_two_pi_mul_I, ←inv_eq_one_div, ←Complex.exp_neg]
  all_goals linarith
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
by_cases h : x ≤ Real.pi / 2
Proof state after:
case pos
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

case neg
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : ¬x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
case pos
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

case neg
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : ¬x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
. calc (2 / Real.pi) * η
  _ ≤ (2 / Real.pi) * x := by gcongr
  _ = (1 - (2 / Real.pi) * x) * Real.sin 0 + ((2 / Real.pi) * x) * Real.sin (Real.pi / 2) := by simp
  _ ≤ Real.sin ((1 - (2 / Real.pi) * x) * 0 + ((2 / Real.pi) * x) * (Real.pi / 2)) := by
    apply (strictConcaveOn_sin_Icc.concaveOn).2 (by simp [Real.pi_nonneg])
    . simp
      constructor <;> linarith [Real.pi_nonneg]
    . rw [sub_nonneg, mul_comm]
      apply mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa)
    . exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) x_nonneg
    . simp
  _ = Real.sin x := by
    congr
    field_simp
  _ ≤ Real.sqrt ((Real.sin x) ^ 2) := by
    rw [Real.sqrt_sq_eq_abs]
    apply le_abs_self
  _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by
      rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
      simp
      rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
      apply (Real.sqrt_le_sqrt_iff _).mpr
      . simp [pow_two_nonneg]
      . linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
Proof state after:
case neg
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : ¬x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
case neg
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : ¬x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
. push_neg at h
  calc (2 / Real.pi) * η
  _ ≤ (2 / Real.pi) * x := by gcongr
  _ = 1 - ((1 - (2 / Real.pi) * (x - Real.pi / 2)) * Real.cos (Real.pi / 2) + ((2 / Real.pi) * (x - Real.pi / 2)) * Real.cos (Real.pi)) := by
    field_simp
    ring
  _ ≤ 1 - (Real.cos ((1 - (2 / Real.pi) * (x - Real.pi / 2)) * (Real.pi / 2) + (((2 / Real.pi) * (x - Real.pi / 2)) * (Real.pi)))) := by
    gcongr
    apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [Real.pi_nonneg])
    . simp
      constructor <;> linarith [Real.pi_nonneg]
    . rw [sub_nonneg, mul_comm]
      apply mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa)
    . exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) (by linarith [h])
    . simp
  _ = 1 - Real.cos x := by
    congr
    field_simp
    ring
  _ ≤ Real.sqrt ((1 - Real.cos x) ^ 2) := by
    rw [Real.sqrt_sq_eq_abs]
    apply le_abs_self
  _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by
      rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
      simp
      rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
      apply (Real.sqrt_le_sqrt_iff _).mpr
      . simp [pow_two_nonneg]
      . linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case pos
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
calc (2 / Real.pi) * η
_ ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (div_nonneg zero_le_two Real.pi_pos.le) ηpos
_ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : η ≤ 0
⊢ 0 ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
apply norm_nonneg
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
convert (@this (-x) _ (by simpa) (by linarith)) using 1
Proof state after:
case h.e'_4
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ ‖1 - (Complex.I * ↑x).exp‖ = ‖1 - (Complex.I * ↑(-x)).exp‖

case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ η ≤ |(-x)|
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ ‖1 - (Complex.I * ↑x).exp‖ = ‖1 - (Complex.I * ↑(-x)).exp‖

case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ η ≤ |(-x)|
Tactic:
. rw [Complex.norm_eq_abs, ←Complex.abs_conj, map_sub, map_one, Complex.ofReal_neg, mul_neg, Complex.norm_eq_abs,
      ←Complex.exp_conj, map_mul, Complex.conj_I, neg_mul, Complex.conj_ofReal]
Proof state after:
case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ η ≤ |(-x)|
Theorem: lower_secant_bound'
Proof state before:
case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ η ≤ |(-x)|
Tactic:
. rwa [abs_neg]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ |(-x)| ≤ 2 * Real.pi - η
Tactic:
simpa
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ 0 ≤ -x
Tactic:
linarith
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ ‖1 - (Complex.I * ↑x).exp‖ = ‖1 - (Complex.I * ↑(-x)).exp‖
Tactic:
rw [Complex.norm_eq_abs, ←Complex.abs_conj, map_sub, map_one, Complex.ofReal_neg, mul_neg, Complex.norm_eq_abs,
    ←Complex.exp_conj, map_mul, Complex.conj_I, neg_mul, Complex.conj_ofReal]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ η ≤ |(-x)|
Tactic:
rwa [abs_neg]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case inr
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
convert (@this (2 * Real.pi - x) _ _ _ _) using 1
Proof state after:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ ‖1 - (Complex.I * ↑x).exp‖ = ‖1 - (Complex.I * ↑(2 * Real.pi - x)).exp‖

case inr.convert_1
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ η ≤ 2 * Real.pi - x

case inr.convert_2
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ 2 * Real.pi - η

case inr.convert_3
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 0 ≤ 2 * Real.pi - x

case inr.convert_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ Real.pi
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ ‖1 - (Complex.I * ↑x).exp‖ = ‖1 - (Complex.I * ↑(2 * Real.pi - x)).exp‖

case inr.convert_1
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ η ≤ 2 * Real.pi - x

case inr.convert_2
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ 2 * Real.pi - η

case inr.convert_3
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 0 ≤ 2 * Real.pi - x

case inr.convert_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ Real.pi
Tactic:
. rw [Complex.norm_eq_abs, ←Complex.abs_conj]
  simp
  rw [←Complex.exp_conj]
  simp
  rw [mul_sub, Complex.conj_ofReal, Complex.exp_sub, mul_comm Complex.I (2 * Real.pi), Complex.exp_two_pi_mul_I, ←inv_eq_one_div, ←Complex.exp_neg]
Proof state after:
case inr.convert_1
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ η ≤ 2 * Real.pi - x

case inr.convert_2
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ 2 * Real.pi - η

case inr.convert_3
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 0 ≤ 2 * Real.pi - x

case inr.convert_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ Real.pi
Theorem: lower_secant_bound'
Proof state before:
case inr.convert_1
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ η ≤ 2 * Real.pi - x

case inr.convert_2
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ 2 * Real.pi - η

case inr.convert_3
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 0 ≤ 2 * Real.pi - x

case inr.convert_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ Real.pi
Tactic:
all_goals linarith
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ ‖1 - (Complex.I * ↑x).exp‖ = ‖1 - (Complex.I * ↑(2 * Real.pi - x)).exp‖
Tactic:
rw [Complex.norm_eq_abs, ←Complex.abs_conj]
Proof state after:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs ((starRingEnd ℂ) (1 - (Complex.I * ↑x).exp)) = ‖1 - (Complex.I * ↑(2 * Real.pi - x)).exp‖
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs ((starRingEnd ℂ) (1 - (Complex.I * ↑x).exp)) = ‖1 - (Complex.I * ↑(2 * Real.pi - x)).exp‖
Tactic:
simp
Proof state after:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs (1 - (starRingEnd ℂ) (Complex.I * ↑x).exp) = Complex.abs (1 - (Complex.I * (2 * ↑Real.pi - ↑x)).exp)
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs (1 - (starRingEnd ℂ) (Complex.I * ↑x).exp) = Complex.abs (1 - (Complex.I * (2 * ↑Real.pi - ↑x)).exp)
Tactic:
rw [←Complex.exp_conj]
Proof state after:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs (1 - ((starRingEnd ℂ) (Complex.I * ↑x)).exp) = Complex.abs (1 - (Complex.I * (2 * ↑Real.pi - ↑x)).exp)
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs (1 - ((starRingEnd ℂ) (Complex.I * ↑x)).exp) = Complex.abs (1 - (Complex.I * (2 * ↑Real.pi - ↑x)).exp)
Tactic:
simp
Proof state after:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs (1 - (-(Complex.I * (starRingEnd ℂ) ↑x)).exp) = Complex.abs (1 - (Complex.I * (2 * ↑Real.pi - ↑x)).exp)
Theorem: lower_secant_bound'
Proof state before:
case h.e'_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ Complex.abs (1 - (-(Complex.I * (starRingEnd ℂ) ↑x)).exp) = Complex.abs (1 - (Complex.I * (2 * ↑Real.pi - ↑x)).exp)
Tactic:
rw [mul_sub, Complex.conj_ofReal, Complex.exp_sub, mul_comm Complex.I (2 * Real.pi), Complex.exp_two_pi_mul_I, ←inv_eq_one_div, ←Complex.exp_neg]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case inr.convert_4
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
this : ∀ {x : ℝ}, η ≤ x → x ≤ 2 * Real.pi - η → 0 ≤ x → x ≤ Real.pi → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_le_pi : ¬x ≤ Real.pi
⊢ 2 * Real.pi - x ≤ Real.pi
Tactic:
linarith
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
case pos
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
calc (2 / Real.pi) * η
_ ≤ (2 / Real.pi) * x := by gcongr
_ = (1 - (2 / Real.pi) * x) * Real.sin 0 + ((2 / Real.pi) * x) * Real.sin (Real.pi / 2) := by simp
_ ≤ Real.sin ((1 - (2 / Real.pi) * x) * 0 + ((2 / Real.pi) * x) * (Real.pi / 2)) := by
  apply (strictConcaveOn_sin_Icc.concaveOn).2 (by simp [Real.pi_nonneg])
  . simp
    constructor <;> linarith [Real.pi_nonneg]
  . rw [sub_nonneg, mul_comm]
    apply mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa)
  . exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) x_nonneg
  . simp
_ = Real.sin x := by
  congr
  field_simp
_ ≤ Real.sqrt ((Real.sin x) ^ 2) := by
  rw [Real.sqrt_sq_eq_abs]
  apply le_abs_self
_ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by
    rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
    simp
    rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
    apply (Real.sqrt_le_sqrt_iff _).mpr
    . simp [pow_two_nonneg]
    . linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 2 / Real.pi * η ≤ 2 / Real.pi * x
Tactic:
gcongr
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 2 / Real.pi * x = (1 - 2 / Real.pi * x) * Real.sin 0 + 2 / Real.pi * x * (Real.pi / 2).sin
Tactic:
simp
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ (1 - 2 / Real.pi * x) * Real.sin 0 + 2 / Real.pi * x * (Real.pi / 2).sin ≤
    ((1 - 2 / Real.pi * x) * 0 + 2 / Real.pi * x * (Real.pi / 2)).sin
Tactic:
apply (strictConcaveOn_sin_Icc.concaveOn).2 (by simp [Real.pi_nonneg])
Proof state after:
case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ Real.pi / 2 ∈ Set.Icc 0 Real.pi

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 0 ≤ 1 - 2 / Real.pi * x

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 0 ≤ 2 / Real.pi * x

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1
Theorem: lower_secant_bound'
Proof state before:
case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ Real.pi / 2 ∈ Set.Icc 0 Real.pi

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 0 ≤ 1 - 2 / Real.pi * x

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 0 ≤ 2 / Real.pi * x

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1
Tactic:
. simp
  constructor <;> linarith [Real.pi_nonneg]
Proof state after:
case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 0 ≤ 1 - 2 / Real.pi * x

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 0 ≤ 2 / Real.pi * x

case a
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
x_le_pi : x ≤ Real.pi
h : x ≤ Real.pi / 2
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1