Theorem: lower_secant_bound' (Carleson/Theorem1_1/Basic.lean)

State before:
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
by_cases ηpos : η ≤ 0
State after:
case pos
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : ¬η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

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‖

case neg
η 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
State after:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : ¬η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

State before:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : ¬η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
push_neg at ηpos
State after:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

State before:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
wlog x_nonneg : 0 ≤ x generalizing x
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
⊢ 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
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

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‖

η : ℝ
η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:
. convert (@this (-x) _ (by simpa) (by linarith)) using 1
  . 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]
  . rwa [abs_neg]
State after:
η : ℝ
η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‖

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:
rw [abs_of_nonneg x_nonneg] at *
State after:
η : ℝ
η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‖

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
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‖

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
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‖

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
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‖

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)]
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‖

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)]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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)|

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]
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)|

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
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

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]
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

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
State after:
no goals

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]
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‖

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
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)

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]
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)

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
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)

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]
State after:
no goals

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
State after:
no goals

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)]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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])
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

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]
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

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
⊢ 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:
. 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)
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 ≤ 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

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
⊢ 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:
. exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) x_nonneg
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
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1

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
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1
Tactic:
. simp
State after:
no goals

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
⊢ 0 ∈ Set.Icc 0 Real.pi
Tactic:
simp [Real.pi_nonneg]
State after:
no goals

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
Tactic:
simp
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 ≤ Real.pi / 2 ∧ 0 ≤ Real.pi

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
⊢ 0 ≤ Real.pi / 2 ∧ 0 ≤ Real.pi
Tactic:
constructor <;> linarith [Real.pi_nonneg]
State after:
no goals

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
⊢ 0 ≤ 1 - 2 / Real.pi * x
Tactic:
rw [sub_nonneg, mul_comm]
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
⊢ x * (2 / Real.pi) ≤ 1

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
⊢ x * (2 / Real.pi) ≤ 1
Tactic:
apply mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa)
State after:
no goals

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
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals

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
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

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
⊢ x ≤ 1 / (2 / Real.pi)
Tactic:
simpa
State after:
no goals

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
⊢ 0 ≤ 2 / Real.pi * x
Tactic:
exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) x_nonneg
State after:
no goals

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
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1
Tactic:
simp
State after:
no goals

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) * 0 + 2 / Real.pi * x * (Real.pi / 2)).sin = x.sin
Tactic:
congr
State after:
case e_x
η : ℝ
η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) * 0 + 2 / Real.pi * x * (Real.pi / 2) = x

State before:
case e_x
η : ℝ
η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) * 0 + 2 / Real.pi * x * (Real.pi / 2) = x
Tactic:
field_simp
State after:
no goals

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
⊢ x.sin ≤ √(x.sin ^ 2)
Tactic:
rw [Real.sqrt_sq_eq_abs]
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
h : x ≤ Real.pi / 2
⊢ x.sin ≤ |x.sin|

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
⊢ x.sin ≤ |x.sin|
Tactic:
apply le_abs_self
State after:
no goals

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
⊢ √(x.sin ^ 2) ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
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
h : x ≤ Real.pi / 2
⊢ √(x.sin ^ 2) ≤ √((1 - ((↑x).cos + (↑x).sin * Complex.I)).re ^ 2 + (1 - ((↑x).cos + (↑x).sin * Complex.I)).im ^ 2)

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
⊢ √(x.sin ^ 2) ≤ √((1 - ((↑x).cos + (↑x).sin * Complex.I)).re ^ 2 + (1 - ((↑x).cos + (↑x).sin * Complex.I)).im ^ 2)
Tactic:
simp
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
h : x ≤ Real.pi / 2
⊢ √(x.sin ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)

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
⊢ √(x.sin ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)
Tactic:
rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
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
h : x ≤ Real.pi / 2
⊢ √(x.sin ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)

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
⊢ √(x.sin ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)
Tactic:
apply (Real.sqrt_le_sqrt_iff _).mpr
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
h : x ≤ Real.pi / 2
⊢ x.sin ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

η : ℝ
η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 - x.cos) ^ 2 + x.sin ^ 2

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
⊢ x.sin ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

η : ℝ
η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 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
. simp [pow_two_nonneg]
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
h : x ≤ Real.pi / 2
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

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
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
. linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
State after:
no goals

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
⊢ x.sin ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
simp [pow_two_nonneg]
State after:
no goals

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
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
State after:
no goals

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
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 : Real.pi / 2 < x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

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 : Real.pi / 2 < x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
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)]
State after:
no goals

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 : Real.pi / 2 < x
⊢ 2 / Real.pi * η ≤ 2 / Real.pi * x
Tactic:
gcongr
State after:
no goals

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 : Real.pi / 2 < x
⊢ 2 / Real.pi * x =
    1 - ((1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2).cos + 2 / Real.pi * (x - Real.pi / 2) * Real.pi.cos)
Tactic:
field_simp
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
h : Real.pi / 2 < x
⊢ 2 * x * (Real.pi * 2) = (Real.pi * 2 + 2 * (x * 2 - Real.pi)) * Real.pi

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 : Real.pi / 2 < x
⊢ 2 * x * (Real.pi * 2) = (Real.pi * 2 + 2 * (x * 2 - Real.pi)) * Real.pi
Tactic:
ring
State after:
no goals

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 : Real.pi / 2 < x
⊢ 1 - ((1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2).cos + 2 / Real.pi * (x - Real.pi / 2) * Real.pi.cos) ≤
    1 - ((1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) * Real.pi).cos
Tactic:
gcongr
State after:
case h
η : ℝ
η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 : Real.pi / 2 < x
⊢ ((1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) * Real.pi).cos ≤
    (1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2).cos + 2 / Real.pi * (x - Real.pi / 2) * Real.pi.cos

State before:
case h
η : ℝ
η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 : Real.pi / 2 < x
⊢ ((1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) * Real.pi).cos ≤
    (1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2).cos + 2 / Real.pi * (x - Real.pi / 2) * Real.pi.cos
Tactic:
apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [Real.pi_nonneg])
State after:
case h.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 : Real.pi / 2 < x
⊢ Real.pi ∈ Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 1 - 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1

State before:
case h.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 : Real.pi / 2 < x
⊢ Real.pi ∈ Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 1 - 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1
Tactic:
. simp
  constructor <;> linarith [Real.pi_nonneg]
State after:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 1 - 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1

State before:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 1 - 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1
Tactic:
. 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)
State after:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1

State before:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 2 / Real.pi * (x - Real.pi / 2)

case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1
Tactic:
. exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) (by linarith [h])
State after:
case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1

State before:
case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1
Tactic:
. simp
State after:
no goals

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 : Real.pi / 2 < x
⊢ Real.pi / 2 ∈ Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)
Tactic:
simp [Real.pi_nonneg]
State after:
no goals

State before:
case h.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 : Real.pi / 2 < x
⊢ Real.pi ∈ Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)
Tactic:
simp
State after:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ Real.pi ∧ 0 ≤ Real.pi / 2

State before:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ Real.pi ∧ 0 ≤ Real.pi / 2
Tactic:
constructor <;> linarith [Real.pi_nonneg]
State after:
no goals

State before:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 1 - 2 / Real.pi * (x - Real.pi / 2)
Tactic:
rw [sub_nonneg, mul_comm]
State after:
case h.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 : Real.pi / 2 < x
⊢ (x - Real.pi / 2) * (2 / Real.pi) ≤ 1

State before:
case h.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 : Real.pi / 2 < x
⊢ (x - Real.pi / 2) * (2 / Real.pi) ≤ 1
Tactic:
apply mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa)
State after:
no goals

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 : Real.pi / 2 < x
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals

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 : Real.pi / 2 < x
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

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 : Real.pi / 2 < x
⊢ x - Real.pi / 2 ≤ 1 / (2 / Real.pi)
Tactic:
simpa
State after:
no goals

State before:
case h.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 : Real.pi / 2 < x
⊢ 0 ≤ 2 / Real.pi * (x - Real.pi / 2)
Tactic:
exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) (by linarith [h])
State after:
no goals

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 : Real.pi / 2 < x
⊢ 0 ≤ x - Real.pi / 2
Tactic:
linarith [h]
State after:
no goals

State before:
case h.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 : Real.pi / 2 < x
⊢ 1 - 2 / Real.pi * (x - Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) = 1
Tactic:
simp
State after:
no goals

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 : Real.pi / 2 < x
⊢ 1 - ((1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) * Real.pi).cos =
    1 - x.cos
Tactic:
congr
State after:
case e_a.e_x
η : ℝ
η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 : Real.pi / 2 < x
⊢ (1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) * Real.pi = x

State before:
case e_a.e_x
η : ℝ
η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 : Real.pi / 2 < x
⊢ (1 - 2 / Real.pi * (x - Real.pi / 2)) * (Real.pi / 2) + 2 / Real.pi * (x - Real.pi / 2) * Real.pi = x
Tactic:
field_simp
State after:
case e_a.e_x
η : ℝ
η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 : Real.pi / 2 < x
⊢ (Real.pi * 2 - 2 * (x * 2 - Real.pi)) * Real.pi * (Real.pi * 2) +
      2 * (x * 2 - Real.pi) * Real.pi * (Real.pi * 2 * 2) =
    x * (Real.pi * 2 * 2 * (Real.pi * 2))

State before:
case e_a.e_x
η : ℝ
η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 : Real.pi / 2 < x
⊢ (Real.pi * 2 - 2 * (x * 2 - Real.pi)) * Real.pi * (Real.pi * 2) +
      2 * (x * 2 - Real.pi) * Real.pi * (Real.pi * 2 * 2) =
    x * (Real.pi * 2 * 2 * (Real.pi * 2))
Tactic:
ring
State after:
no goals

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 : Real.pi / 2 < x
⊢ 1 - x.cos ≤ √((1 - x.cos) ^ 2)
Tactic:
rw [Real.sqrt_sq_eq_abs]
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
h : Real.pi / 2 < x
⊢ 1 - x.cos ≤ |1 - x.cos|

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 : Real.pi / 2 < x
⊢ 1 - x.cos ≤ |1 - x.cos|
Tactic:
apply le_abs_self
State after:
no goals

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 : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
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
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤
    √((1 - ((↑x).cos + (↑x).sin * Complex.I)).re ^ 2 + (1 - ((↑x).cos + (↑x).sin * Complex.I)).im ^ 2)

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 : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤
    √((1 - ((↑x).cos + (↑x).sin * Complex.I)).re ^ 2 + (1 - ((↑x).cos + (↑x).sin * Complex.I)).im ^ 2)
Tactic:
simp
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
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)

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 : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)
Tactic:
rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
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
h : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)

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 : Real.pi / 2 < x
⊢ √((1 - x.cos) ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)
Tactic:
apply (Real.sqrt_le_sqrt_iff _).mpr
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
h : Real.pi / 2 < x
⊢ (1 - x.cos) ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

η : ℝ
η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 : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

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 : Real.pi / 2 < x
⊢ (1 - x.cos) ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

η : ℝ
η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 : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
. simp [pow_two_nonneg]
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
h : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2

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 : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
. linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
State after:
no goals

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 : Real.pi / 2 < x
⊢ (1 - x.cos) ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
simp [pow_two_nonneg]
State after:
no goals

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 : Real.pi / 2 < x
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
State after:
no goals