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

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
by_cases ηpos : η < 0
State after:
case pos
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)

case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)

State before:
case pos
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)

case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
. calc η / 2
  _ ≤ 0 := by linarith
  _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg
State after:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)

State before:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : ¬η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
push_neg at ηpos
State after:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)

State before:
case neg
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
calc η / 2
_ ≤ (2 / Real.pi) * η := by
  ring_nf
  rw [mul_assoc]
  gcongr
  field_simp
  rw [div_le_div_iff (by norm_num) Real.pi_pos]
  linarith [Real.pi_le_four]
_ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
  apply lower_secant_bound' xAbs
  rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]
  exact xIcc
State after:
no goals

State before:
case pos
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ Complex.abs (1 - (Complex.I * ↑x).exp)
Tactic:
calc η / 2
_ ≤ 0 := by linarith
_ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg
State after:
no goals

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ η / 2 ≤ 0
Tactic:
linarith
State after:
no goals

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : η < 0
⊢ 0 ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
apply norm_nonneg
State after:
no goals

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η / 2 ≤ 2 / Real.pi * η
Tactic:
ring_nf
State after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * Real.pi⁻¹ * 2

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * Real.pi⁻¹ * 2
Tactic:
rw [mul_assoc]
State after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * (Real.pi⁻¹ * 2)

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ η * (1 / 2) ≤ η * (Real.pi⁻¹ * 2)
Tactic:
gcongr
State after:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ Real.pi⁻¹ * 2

State before:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ Real.pi⁻¹ * 2
Tactic:
field_simp
State after:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ 2 / Real.pi

State before:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 / 2 ≤ 2 / Real.pi
Tactic:
rw [div_le_div_iff (by norm_num) Real.pi_pos]
State after:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 * Real.pi ≤ 2 * 2

State before:
case h
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 1 * Real.pi ≤ 2 * 2
Tactic:
linarith [Real.pi_le_four]
State after:
no goals

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
apply lower_secant_bound' xAbs
State after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ |x| ≤ 2 * Real.pi - η

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ |x| ≤ 2 * Real.pi - η
Tactic:
rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]
State after:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ -2 * Real.pi + η ≤ x ∧ x ≤ 2 * Real.pi - η

State before:
η x : ℝ
xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)
xAbs : η ≤ |x|
ηpos : 0 ≤ η
⊢ -2 * Real.pi + η ≤ x ∧ x ≤ 2 * Real.pi - η
Tactic:
exact xIcc
State after:
no goals