Dealing with inequalities

Stream: new members

[Christian K]

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic


noncomputable abbrev sq_2 := Real.sqrt 2
example : -(1 / 2) ≤ 1 / 2 * Real.cos (↑n * sq_2) := by
  sorry


example : Real.sin (↑n * sq_2) * Real.sin sq_2 * (-1 / 2) ≤
      1 / 2 + Real.cos (↑n * sq_2) * Real.cos sq_2 * (1 / 2) := by
  sorry

I want to prove these two inequalites, but I have no idea how to simplify them. With equalities I would use apply_fun to simplify the expression, but this does not work for <=. It says that I need to prove that the function I'm using is monotone but I have no idea how.
Do you have some general tips about proving such inequalities?

[Jireh Loreaux]

For the first you should use docs#Real.neg_one_le_cos

[Christian K]

Yeah, I know about this, but how do i get rid of the 1/2?

[Jireh Loreaux]

gcongr is a handy tactic for this kind of thing:

example : -(1 / 2) ≤ 1 / 2 * Real.cos (↑n * sq_2) := by
  calc
    -(1 / 2) ≤ (1 / 2) * (-1) := by simp
    _ ≤ (1 / 2) * (Real.cos (n * sq_2)) := by
      gcongr
      exact Real.neg_one_le_cos (n * sq_2)

[Jireh Loreaux]

Also, what is the type of n supposed to be? With autoimplicits on, Lean assumes it to be ℝ, but you have a ↑ in your statement. Is n supposed to have type ℕ?

[Christian K]

Ohh, i forgot to include this in the mwe, you guessed it correctly, n is supposed to have type Nat.

[Christian K]

And how about the second lemma, I don't really see how i should use a calc proof with the gcongr tactic to solve it?

[Christian K]

lemma sin_le_cos (x : Real) : Real.sin x ≤ 1 + Real.cos x := by
  sorry

could a lemma like this help?

[Jireh Loreaux]

that inequality is not true.

[Jireh Loreaux]

Take x := -π/3

[Jireh Loreaux]

Your second result follows from the angle addition formula docs#Real.cos_sub

[Christian K]

Ohh ok, thank you, I figured it out