# 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: May 10 2021 at 23:11 UTC