Quadratic equations

Stream: Is there code for X?

[Rémy Degenne]

What do we have in Mathlib to find extremal values of real quadratic functions?
I need those two lemmas and don't know which tools we have to make their proofs as quick as possible:

import Mathlib

lemma quadratic_inequality {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt_one : δ < 1) (u : ℝ) :
    (1 - u * δ) * (1 + u * (1 - δ)) ≤ (1 - δ)⁻¹ * δ⁻¹ * 4⁻¹ := by
  sorry

lemma simpler_inequality (δ : ℝ) :
    (1 - δ) * δ ≤ 1 / 4 := by
  sorry

[Kevin Buzzard]

lemma simpler_inequality (δ : ℝ) :
    (1 - δ) * δ ≤ 1 / 4 := by
  have : (δ - 1/2)^2 ≥ 0 := by positivity
  linear_combination this

[Yaël Dillies]

You just need to tell linarith the magic number:

lemma simpler_inequality {δ : ℝ} : (1 - δ) * δ ≤ 1 / 4 := by
  linarith [sq_nonneg (1 / 2 - δ)]

[Rémy Degenne]

Thanks! It looks like it's time for me to learn about linear_combination. And for the other one I guess I first put it into a similar form and then proceed with that kind of proof.

[Rémy Degenne]

Greedy question: could someone be tempted into writing a tactic that optimizes quadratic functions? :D

[Kenny Lau]

if you want to learn how to write tactic i'll personally answer your questions

[Rémy Degenne]

Learning to write tactics has been on my todo list for a while, but I'm afraid I still won't take the time to do it today.

[Oliver Nash]

I can't help here but you might improve your odds of tempting a tactic writer if you threw together a handful of units tests and pasted them in this thread.

[František Silváši 🦉]

I can't help here but you might improve your odds of tempting a tactic writer if you threw together a handful of units tests and pasted them in this thread.

I promise to have a look if this exists :).

[Kevin Buzzard]

import Mathlib

lemma quadratic_inequality {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt_one : δ < 1) (u : ℝ) :
    (1 - u * δ) * (1 + u * (1 - δ)) ≤ (1 - δ)⁻¹ * δ⁻¹ * 4⁻¹ := by
  have : 0 < 1 - δ := by linarith -- need in context for `field_simp`
  have : -(u - (δ⁻¹ - (1-δ)⁻¹)/2)^2 ≤ 0 := by simp; positivity -- complete square
  linear_combination (norm := skip) δ * (1 - δ) * this -- u^2 and u terms now cancel
  field_simp -- clear denominators
  ring_nf -- tidy up but it's an inequality not an equality so `ring` doesn't work
  norm_num -- only numerals left

[Kevin Buzzard]

Shout out to @Heather Macbeth for teaching me both norm := skip and use of ring_nf after field_simp in her "golf club" lecture on Tuesday!

[Heather Macbeth]

Couple more tricks on Kevin's solution:

lemma quadratic_inequality {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt_one : δ < 1) (u : ℝ) :
    (1 - u * δ) * (1 + u * (1 - δ)) ≤ (1 - δ)⁻¹ * δ⁻¹ * 4⁻¹ := by
  have : 0 < 1 - δ := by linarith -- need in context for `field_simp`
  have : 0 ≤ (u - (δ⁻¹ - (1-δ)⁻¹)/2)^2 := by positivity -- complete square
  field_simp at this ⊢
  linear_combination this -- or `linarith`

[Alex Kontorovich]

So maybe my question should apply here: could

have : 0 < 1 - δ := by linarith -- need in context for `field_simp`

be done within field_simp (since it appears with a ⁻¹)?

[Heather Macbeth]

Again that's a question for positivity, not field_simp :)

[Heather Macbeth]

(But the answer is no ... positivity is lightweight and can't call linarith which is heavy)

[Michael Rothgang]

Can bound prove this?

[Alex Kontorovich]

(Does field_simp call bound?)

[Michael Rothgang]

(No, it doesn't - but you can make it so by using the disch option.)

[Heather Macbeth]

Alex Kontorovich said:

(Does field_simp call bound?)

Do you mean, does positivity call bound?

[Alex Kontorovich]

Michael Rothgang said:

(No, it doesn't - but you can make it so by using the disch option.)

Ah! Maybe that's what I've been missing! (This is for the Real Analysis Game...) I'll try it, thanks!

[Rémy Degenne]

Wow, thanks for the golfs! I had written a proof starting with the same two lines as the one of Heather, but it was nowhere near as concise afterwards!
field_simp with a bound discharger works without the positivity hint:

import Mathlib

lemma quadratic_inequality {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt_one : δ < 1) (u : ℝ) :
    (1 - u * δ) * (1 + u * (1 - δ)) ≤ (1 - δ)⁻¹ * (δ⁻¹ * 4⁻¹) := by
  have : 0 ≤ (u - (δ⁻¹ - (1-δ)⁻¹)/2)^2 := by positivity -- complete square
  field_simp (disch := bound) at this ⊢ -- clear denominators
  linarith

[Yaël Dillies]

Here's my take:

import Mathlib

lemma quadratic_inequality {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt_one : δ < 1) (u : ℝ) :
    (1 - u * δ) * (1 + u * (1 - δ)) ≤ (1 - δ)⁻¹ * (δ⁻¹ * 4⁻¹) := by
  field_simp (disch := bound) at this ⊢ -- clear denominators
  linarith [sq_nonneg  (u - (δ⁻¹ - (1-δ)⁻¹)/2)] -- complete square

[Heather Macbeth]

The other major systems have a "sum of squares" tactic, originating in this paper of Harrison. I believe it would invent the relevant sum of squares, with no input from the user, so the proof would be just

lemma quadratic_inequality {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt_one : δ < 1) (u : ℝ) :
    (1 - u * δ) * (1 + u * (1 - δ)) ≤ (1 - δ)⁻¹ * δ⁻¹ * 4⁻¹ := by
  field_simp [sub_pos.2 hδ_lt_one]
  sos

[Kevin Buzzard]

Perhaps nlinarith could be adapted to figure out some good sums of squares?

[metakuntyyy]

Rémy Degenne said:

Greedy question: could someone be tempted into writing a tactic that optimizes quadratic functions? :D

I'd like to write a tactic if I know what's the tactic supposed to do.

[Aaron Liu]

Oliver Nash said:

I can't help here but you might improve your odds of tempting a tactic writer if you threw together a handful of units tests and pasted them in this thread.

I'd like to write a tactic if I can know the scope of what it's supposed to do

[Kevin Buzzard]

@Rémy Degenne another thing Heather has taught me is that the way to write a tactic is to start simply by stating a bunch of theorems which you think should be solved by the tactic. So this is the first step.

[Heather Macbeth]

@metakuntyyy @Aaron Liu If you're seriously interested in this, the right way to do it is to port Harrison's tactic. But it's a big project.

[metakuntyyy]

Ah I see. I'm looking to learn some easy metaprogramming as I don't have that much experience with it. Not sure if I'm capable taking a big metaproject yet.

@Kim Morrison has said in a thread that I can't find that there are some simprocs missing. Maybe those are simpler to do.

[František Silváši 🦉]

@Heather Macbeth What's this 'Harrison's tactic' in reference to here :)?

[Kevin Buzzard]

See this message in this thread.

[Vasilii Nesterov]

I've been interested in porting Harrison's tactic for a long time. But it's indeed a difficult task

[František Silváši 🦉]

Yeah the:

So instead we postulate that the “exact” solutions probably involve rational numbers with moderate coefficients, and try rounding all the values based on common denominators 1, 2, 3, .... (Once we reach 32 we start to go up by a multiple of 2 each time.)

bit makes me wonder if this is really the best way to approach this :sweat_smile:.