internlm/Lean-Github huggingface dataset:
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
⊢ 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)
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 ≤ 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
⊢ 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
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
⊢ 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
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1
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
⊢ 0 ∈ Set.Icc 0 Real.pi
Tactic:
simp [Real.pi_nonneg]
Proof state after:
no goals
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
Tactic:
simp
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 ≤ Real.pi / 2 ∧ 0 ≤ Real.pi
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
⊢ 0 ≤ Real.pi / 2 ∧ 0 ≤ Real.pi
Tactic:
constructor <;> linarith [Real.pi_nonneg]
Proof state after:
no goals
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
⊢ 0 ≤ 1 - 2 / Real.pi * x
Tactic:
rw [sub_nonneg, mul_comm]
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
⊢ x * (2 / Real.pi) ≤ 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
⊢ 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)
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
⊢ 0 ≤ 1
Tactic:
norm_num
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
⊢ 0 ≤ 2
Tactic:
norm_num
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
⊢ x ≤ 1 / (2 / Real.pi)
Tactic:
simpa
Proof state after:
no goals
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
⊢ 0 ≤ 2 / Real.pi * x
Tactic:
exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) x_nonneg
Proof state after:
no goals
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
⊢ 1 - 2 / Real.pi * x + 2 / Real.pi * x = 1
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) * 0 + 2 / Real.pi * x * (Real.pi / 2)).sin = x.sin
Tactic:
congr
Proof 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
Theorem: lower_secant_bound'
Proof 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
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
⊢ x.sin ≤ √(x.sin ^ 2)
Tactic:
rw [Real.sqrt_sq_eq_abs]
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
h : x ≤ Real.pi / 2
⊢ x.sin ≤ |x.sin|
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
⊢ x.sin ≤ |x.sin|
Tactic:
apply le_abs_self
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
⊢ √(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]
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
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)
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
⊢ √(x.sin ^ 2) ≤ √((1 - ((↑x).cos + (↑x).sin * Complex.I)).re ^ 2 + (1 - ((↑x).cos + (↑x).sin * Complex.I)).im ^ 2)
Tactic:
simp
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
h : x ≤ Real.pi / 2
⊢ √(x.sin ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)
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
⊢ √(x.sin ^ 2) ≤ √((1 - (↑x).cos.re) ^ 2 + (↑x).sin.re ^ 2)
Tactic:
rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
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
h : x ≤ Real.pi / 2
⊢ √(x.sin ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)
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
⊢ √(x.sin ^ 2) ≤ √((1 - x.cos) ^ 2 + x.sin ^ 2)
Tactic:
apply (Real.sqrt_le_sqrt_iff _).mpr
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
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
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
⊢ 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]
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
h : x ≤ Real.pi / 2
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
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
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
. 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
⊢ x.sin ^ 2 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
simp [pow_two_nonneg]
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
⊢ 0 ≤ (1 - x.cos) ^ 2 + x.sin ^ 2
Tactic:
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 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
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 : Real.pi / 2 < x
⊢ 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 : 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)]
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 : Real.pi / 2 < x
⊢ 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 : 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
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
h : Real.pi / 2 < x
⊢ 2 * x * (Real.pi * 2) = (Real.pi * 2 + 2 * (x * 2 - Real.pi)) * Real.pi
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 : Real.pi / 2 < x
⊢ 2 * x * (Real.pi * 2) = (Real.pi * 2 + 2 * (x * 2 - Real.pi)) * Real.pi
Tactic:
ring
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 : 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
Proof 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
Theorem: lower_secant_bound'
Proof 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])
Proof 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
Theorem: lower_secant_bound'
Proof 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]
Proof 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
Theorem: lower_secant_bound'
Proof 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)
Proof 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
Theorem: lower_secant_bound'
Proof 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])
Proof 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
Theorem: lower_secant_bound'
Proof 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
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 : Real.pi / 2 < x
⊢ Real.pi / 2 ∈ Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)
Tactic:
simp [Real.pi_nonneg]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof 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
Proof 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
Theorem: lower_secant_bound'
Proof 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]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof 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]
Proof 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
Theorem: lower_secant_bound'
Proof 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)
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 : Real.pi / 2 < x
⊢ 0 ≤ 1
Tactic:
norm_num
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 : Real.pi / 2 < x
⊢ 0 ≤ 2
Tactic:
norm_num
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 : Real.pi / 2 < x
⊢ x - Real.pi / 2 ≤ 1 / (2 / Real.pi)
Tactic:
simpa
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof 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])
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 : Real.pi / 2 < x
⊢ 0 ≤ x - Real.pi / 2
Tactic:
linarith [h]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof 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
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 : 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
Proof 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
Theorem: lower_secant_bound'
Proof 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
Proof 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))
Theorem: lower_secant_bound'
Proof 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
Proof state after:
no goals