How prove the example like this

Stream: new members

[Marcus]

Let f(x) = sinx or another function, take

$$x \in \pi /4 \to \pi /2$$

How to prove

$$\mid f(x) \mid \leq 1$$

that use lean4 .

I rewrite this example to lean4 form like this:

example (f:ℝ → ℝ )(h:∀ x, f x = sin x) : ∀ x ∈ Set.Icc (π /4) (π /2) , f x ∈ Set.Icc  (\sqrt 2 * 1/2) 1:= by
   sorry

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

@loogle Real.sin, LE.le, 1

[loogle]

:search: Real.sin_le_one, Real.neg_one_le_sin, and 18 more

[Kevin Buzzard]

The first two hits do it

[Kevin Buzzard]

As for the lower bound, what's your maths proof? Note that "it's obvious from the picture" is not a proof.

[Marcus]

Kevin Buzzard 发言道：

The first two hits do it

thanks for you reply , I just give a simple example . Actually, the situation is more complicated, the function like a sin (\pi/3+x) - cos(x) . It looks like composite function of elementary functions. I hope some hits to help me prove that use lean4

[Kevin Buzzard]

Well you have to give the maths proof first -- lean does not do magic. To make progress here I suggest you ask a concrete question in maths, give a maths answer, and also give the question in lean formulated as a #mwe with a sorry. That is the best way to ask questions here. Right now your questions are too vague, you're just saying you have a complicated question without saying what it is.

[Kevin Buzzard]

For the example you gave above involving $\sqrt{2}/2$, you should make it a #mwe and then give the maths proof which you want to formalise, and then we can make progress.

[Marcus]

Kevin Buzzard 发言道：

For the example you gave above involving $\sqrt{2}/2$, you should make it a #mwe and then give the maths proof which you want to formalise, and then we can make progress.

Thanks ,That's my problem. I will make it better

[Ilmārs Cīrulis]

import Mathlib

example: ∀ x ∈ Set.Icc (Real.pi / 4) (Real.pi / 2), Real.sin x ∈ Set.Icc (√ 2 / 2) 1 := by
   sorry

@Marcus How does this possible #mwe look to you?

[Kevin Buzzard]

But the big question is: which proof is to be formalized? I'll say again -- "it's obvious from the picture" is not a proof.

[Kevin Buzzard]

@loogle Real.sin, Real.pi / 4

[loogle]

:search: Real.sin_pi_div_four

[Kevin Buzzard]

That's a good start, but there's still some work to be done.

[Ilmārs Cīrulis]

I would suggest the proof that uses strict monotonicity in the interval [-pi/2, pi/2] and also values of sine at the specific values... smth like that.

[Ilmārs Cīrulis]

@loogle Real.sin "mono"

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

@loogle Real.sin, StrictMono

[loogle]

:shrug: nothing found

[Kevin Buzzard]

It's @**loogle**

[Kevin Buzzard]

@loogle Real.sin, "mono"

[loogle]

:search: Real.strictMonoOn_sin

[Ilmārs Cīrulis]

Real.strictMonoOn_sin

[Kevin Buzzard]

OK now it's easy :-)

[Ilmārs Cīrulis]

Thank you! Now I know how to use loogle. :)

[Kevin Buzzard]

(in the sense that we don't need to find any more library results, it's just a case of putting all the pieces together)

[Ilmārs Cīrulis]

import Mathlib

example: ∀ x ∈ Set.Icc (Real.pi / 4) (Real.pi / 2), Real.sin x ∈ Set.Icc (√ 2 / 2) 1 := by
   intro x Hx
   constructor
   . have H0: x = Real.pi / 4 ∨ Real.pi / 4 < x := by
       sorry
     obtain H0 | H0 := H0
     . rw [H0]
       simp
     . apply Real.strictMonoOn_sin at H0
       . simp at *
         sorry
       . simp at *
         sorry
       . simp at *
         sorry
   . exact Real.sin_le_one x

I left few sorry here, but the skeleton is ready.

[Ilmārs Cīrulis]

There should be some tactic for such inequalities on real numbers, probably, which I simply don't know yet.

[Ilmārs Cīrulis]

Ok, I did it, although not sure if it's the best/shortest way to do it.

import Mathlib

example: ∀ x ∈ Set.Icc (Real.pi / 4) (Real.pi / 2), Real.sin x ∈ Set.Icc (√ 2 / 2) 1 := by
   intro x Hx
   constructor
   . have H0: x = Real.pi / 4 ∨ Real.pi / 4 < x := by
       simp at *
       obtain ⟨Hx, Hx0⟩ := Hx
       exact Or.symm (LE.le.gt_or_eq Hx) -- suggested by exact?
     obtain H0 | H0 := H0
     . rw [H0]
       simp
     . apply Real.strictMonoOn_sin at H0
       . simp at *
         exact le_of_lt H0
       . simp at *
         constructor
         . linarith
         . linarith
       . simp at *
         constructor
         . linarith
         . linarith
   . exact Real.sin_le_one x

[Michael Stoll]

Here is a more compact way.

import Mathlib

example: ∀ x ∈ Set.Icc (Real.pi / 4) (Real.pi / 2), Real.sin x ∈ Set.Icc (√ 2 / 2) 1 := by
  intro x Hx
  simp only [Set.mem_Icc] at Hx
  refine ⟨?_, Real.sin_le_one x⟩
  rw [← Real.sin_pi_div_four]
  refine Real.strictMonoOn_sin.monotoneOn ?_ ?_ Hx.1 <;>
    (constructor <;> linarith)

(admittedly somewhat obscure in the last two lines...)

[Ilmārs Cīrulis]

I took some stuff from you and shortened mine too a bit, while trying to remain beginner friendly.

import Mathlib

example: ∀ x ∈ Set.Icc (Real.pi / 4) (Real.pi / 2), Real.sin x ∈ Set.Icc (√ 2 / 2) 1 := by
   intro x Hx
   refine ⟨?_, Real.sin_le_one x⟩
   have H0: Real.pi / 4 < x ∨ x = Real.pi / 4 := by
     exact LE.le.gt_or_eq Hx.1 -- suggested by exact?
   obtain H0 | H0 := H0
   . apply Real.strictMonoOn_sin at H0 <;> simp at *
     . linarith
     . constructor <;> linarith
     . constructor <;> linarith
   . simp [H0]

[Michael Stoll]

Note that I used Real.strictMonoOn_sin.monotoneOn, which is short for StrictMonoOn.monotoneOn Real.strictMonoOn_sin; it converts the strict monotonicity statement to ordinary monotonicity, so you can work with non-strict instead of strict inequalities. This simplifies the argument a bit (for example, there is no need for the case split via H0).

[Ilmārs Cīrulis]

Yes, that one is really useful.

[Ilmārs Cīrulis]

Why would one use Set.Icc instead of ordinary inequalities?

[Kevin Buzzard]

exact? tends not to use dot notation: you can replace exact LE.le.gt_or_eq Hx.1 with exact Hx.1.gt_or_eq because Hx.1 : Real.pi / 4 ≤ x so it has type LE.le <something>

[Kevin Buzzard]

Lessness said:

Why would one use Set.Icc instead of ordinary inequalities?

import Mathlib

open Real

example (x : ℝ) : x ∈ Set.Icc (π / 4) (π / 2) ↔ π / 4 ≤ x ∧ x ≤ π / 2 := by
  rfl -- it's the same thing, it's just notation

[Ilmārs Cīrulis]

Thank you!

[Ruben Van de Velde]

Though not "notation" as lean understands it

[Kevin Buzzard]

Yes, that was a poor choice of words

[Kevin Buzzard]

But it is the same thing in the sense of definitionally equal

[Ilmārs Cīrulis]

Is there any difference between π and Real.pi? Because if I replace the second with the first, my proof stops working.

Like this (which fails):

import Mathlib

example (x: ℝ) (Hx: x ∈ Set.Icc (π / 4) (π / 2)): Real.sin x ∈ Set.Icc (√ 2 / 2) 1 := by
   refine ⟨?_, Real.sin_le_one x⟩
   rw [<- Real.sin_pi_div_four]
   refine Real.strictMonoOn_sin.monotoneOn ?_ ?_ Hx.left <;> simp at * <;> (constructor <;> linarith)

[Michael Stoll]

If you open Real first, then you can use π (this is notation in the Lean sense for Real.pi).