Zulip Chat Archive

Stream: new members

Topic: How do I go from < to ≤

YH (Dec 12 2019 at 06:33):

If we have a < b := a ≤ b ∧ ¬ (b ≤ a) and h : a < b can I just have h1 : a ≤ b := h.left? (Doesn't seem to work.)

YH (Dec 12 2019 at 06:39):

I'm aware of le_of_lt but I'm still curious about why h.left won't do.

Johan Commelin (Dec 12 2019 at 06:41):

Does change a ≤ b ∧ ¬ (b ≤ a) at h work?

Johan Commelin (Dec 12 2019 at 06:42):

If not, then I'm afraid that in your context the definition of < might be something else.

Johan Commelin (Dec 12 2019 at 06:42):

I would need a MWE to help further.

YH (Dec 12 2019 at 06:51):

Does change a ≤ b ∧ ¬ (b ≤ a) at h work?

pasted image
Doesn't seem to work in this toy case.

YH (Dec 12 2019 at 06:53):

I tried ℕ, ℚ, ℝ it seems change only work for ℚ

Johan Commelin (Dec 12 2019 at 06:57):

So I guess that means that ≤ is not defined the way you think it is.

Kevin Buzzard (Dec 12 2019 at 07:01):

IIRC the definition of < on nat is something like succ a.<= b

YH (Dec 12 2019 at 07:02):

OK.

YH (Dec 12 2019 at 07:03):

Is the AM-GM inequality proved anywhere in mathlib? I was trying this as an exercise, still lots of frustrations

Mario Carneiro (Dec 12 2019 at 07:05):

There is a theorem that says a < b <-> a ≤ b ∧ ¬ (b ≤ a) baked into the definition of preorder, but it is not a definition, it is a constraint on implementations. The actual definition is provided by the particular structure, and many structures have different definitions for this, for example succ a <= b for nat

Mario Carneiro (Dec 12 2019 at 07:06):

If you leave the definition out when defining a preorder, the default definition is a < b := a ≤ b ∧ ¬ (b ≤ a)

Kevin Buzzard (Dec 12 2019 at 07:37):

I don't recall seeing AM-GM in mathlib, there is a relatively straightforward proof using square roots and the sqrt API is good enough to make implementation not too hard.

YH (Dec 12 2019 at 07:41):

Doesn't AM-GM need an nth root API?

Kevin Buzzard (Dec 12 2019 at 07:42):

Oh for n variables?

YH (Dec 12 2019 at 07:42):

Yeah.

Kevin Buzzard (Dec 12 2019 at 07:42):

I'm not sure I know which proof to formalise for n variables. There's a proof that does powers of 2 first and deduces the general case

YH (Dec 12 2019 at 07:43):

That is the one I had in mind. But for that one needs to prove some general induction stuff I guess.

YH (Dec 12 2019 at 07:44):

But even to go from AG4 to AG3 is kinda painful for me right now.

Kevin Buzzard (Dec 12 2019 at 07:45):

I don't remember the trick. Do you let the dummy variable be the GM?

YH (Dec 12 2019 at 07:46):

Yeah. apply AM-GM for a,b,c,d where d = 3√(abc)

Kevin Buzzard (Dec 12 2019 at 07:49):

import data.real.basic

open real

theorem AG2 (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt (x * y) ≤ (x + y) / 2 :=
begin
  have h : 0 ≤ (sqrt x - sqrt y) * (sqrt x - sqrt y),
    apply mul_self_nonneg,
  rw [mul_sub, sub_mul, sub_mul, ←sqrt_mul hx, ←sqrt_mul hx,
      ←sqrt_mul hy, ←sqrt_mul hy, sqrt_mul_self hx, sqrt_mul_self hy, mul_comm] at h,
  linarith,
end

There's 2 ;-) Sorry, I thought that was what we were talking about at first.

YH (Dec 12 2019 at 07:49):

I was trying lemma ag3 (a b c : nnreal) : 3 * (a * b * c) ≤ a ^ 3 + b ^ 3 + c ^ 3 := sorry
but it seems I will have to write instance : has_pow nnreal ℚ anyway.

Kevin Buzzard (Dec 12 2019 at 07:50):

I don't know how well developed things like nnreal are. Does linarith work with them?

Kevin Buzzard (Dec 12 2019 at 07:50):

I just stuck to the reals and put non-negativity hypotheses in.

YH (Dec 12 2019 at 07:52):

Oh, OK. put non-negativity hypotheses in sounds good.
(But still need to define has_pow somewhere I guess.)

YH (Dec 12 2019 at 07:55):

I don't remember the trick. Do you let the dummy variable be the GM?

BTW let the dummy variable be AM works too. But neither seem completely trivial for me as a beginner -- I always got stuck on some seemingly very trivial algebraic operation in Lean.

Kevin Buzzard (Dec 12 2019 at 07:55):

I agree that proving it for n variables is a tall order in lean for a beginner

Yury G. Kudryashov (Dec 13 2019 at 00:38):

I think that the proper way to prove this inequality is to prove https://en.wikipedia.org/wiki/Jensen%27s_inequality

Yury G. Kudryashov (Dec 13 2019 at 00:47):

This way we can (a) assign weights to variables; (b) prove that the square mean is greater than the arithmetic mean; (c) if/once we prove that the center of mass of a measure supported on a convex set belongs to this set, we can have integral versions of these inequalities.

Last updated: Dec 20 2023 at 11:08 UTC