struggling to find maths strategy to show inequality

Stream: new members

[rzeta0]

I've spent 2 days and can't make progress with the maths behind this exercise, hence I'm asking here. Note: this question is more about a mathematical strategy than it is about lean coding

The exercise is to complete:

example {n : ℤ} : ∃ a, 2 * a ^ 3 ≥ n * a + 7 := by
    sorry

Interpretation
My interpretation of this is: Find an example of a such that for all n : ℤ the condition 2*a^3 ≥ n*a + 7 holds. Tell me if my interpretation is wrong.

Getting Started
Heuristically, the exponent of the LHS should match the exponent of the RHS. This leads me to a=n^2+k. By plotting graphs of the RHS-LHS https://www.desmos.com/calculator/e8jlpq4mr2 and adjusting values of k, I find that a=n^2+2 should work.

Next is to prove this.

Strategy 1
I previously learned that "completing the square" is useful in Lean because it has the built in extra tactic, well, Heather MacBeth's course does. For this algebra, I just can't find a suitable completion of the square.

Strategy 2
I then considered term by term comparisons. I can eliminate the 2*n^6 term using extra. I then run into showing the 12*n^4 term is greater than or equal to the n^3 term but this doesn't seem easy in Lean. Similarly, 24*n^2 ≥ 2*n doesn't seem easy in lean.

Non-lean Strategy
If I wasn't following a Lean course, I'd probably do this analytically by finding the minimum of. the RHS-LHS and then showing it is more than zero at this point, and then also showing the second derivative is positive, so RHS-LHS never goes negative. Something like that.

i did think about splitting into cases n ≤ 0 ∨ 1 ≤ n but again, no easy path.

Any suggestions, pointers?

[Etienne Marion]

rzeta0 said:

My interpretation of this is: Find an example of a such that for all n : ℤ the condition 2*a^3 ≥ n*a + 7 holds. Tell me if my interpretation is wrong.

The order of the quantifier is wrong here. For all n you have to provide some a which satisfies the condition, so a is allowed to depend on n.

[Daniel Weber]

a = max n 2 should work

[Daniel Weber]

(deleted)

[A.]

I did get a case split to work with

obtain h | h := le_or_gt n 9
· use 3
  ...
· use -1
  ...

but the neater solution does indeed use n ^ 2 + 2. If you can find the appropriate intermediate expression it should take you just one application of extra and one application of ring to prove that

0 ≤ 2 * (2 * (n ^ 2 + 2) ^ 3 - n * (n ^ 2 + 2) - 7)

[rzeta0]

thanks @A. i will keep searching for that intermediate expression that has eludes me if you think it exists.

also thanks @Etienne Marion - I am new to quantifiers and your correction is appreciated.

[rzeta0]

actually after a couple more hours I still can't find it - any pointers welcome

[rzeta0]

Here's my eventual solution thanks to a hint from @A. ...

my solution is so ugly!

I realise I'm only a beginner but I do feel such exercises don't teach anything about lean concepts, and are merely algebra torture with not much educational value.

Am i wrong? Should I be taking some lesson from this exercise about proofs or formulating lean proofs?

example {n : ℤ} : ∃ a, 2 * a ^ 3 ≥ n * a + 7 := by
  -- have h1 : 2*(n^2+2)^3 = 2*n^6 + 12*n^4 + 24*n^2 + 16 := by ring
  -- have h2 : n*(n^2 + 2) + 7 = n^3 + 2*n + 7 := by ring
  -- have h3 : (n-1)^2*(n^2+2) = n^4 - 2*n^3 + 3*n^2 - 4*n + 2 := by ring
  --
  have h4 := by
    calc
      2*(n^2+2)^3*2 = 4*n^6 + 24*n^4 + 48*n^2 + 32 := by ring
      _ = 4*n^6 + (n-1)^2*(n^2+2) + 23*n^4 + 2*n^3 + 45*n^2 +4*n + 30 := by ring
      _ ≥ (n-1)^2*(n^2+2) + 23*n^4 + 2*n^3 + 45*n^2 +4*n + 30 := by extra
      _ ≥ 23*n^4 + 2*n^3 + 45*n^2 +4*n + 30 := by extra
      _ ≥ 2*n^3 + 45*n^2 +4*n + 30 := by extra
      _ ≥ 2*n^3 + 4*n + 30 := by extra
      _ = (n^3 + 2*n + 15)*2 := by ring
  cancel 2 at h4
  --
  use n^2 + 2
  --
  calc
    2 * (n ^ 2 + 2) ^ 3 ≥ n ^ 3 + 2 * n + 15 := by rel [h4]
    _ = n * (n^2 + 2) + 7 + 8 := by ring
    _ ≥ n * (n^2 + 2) + 7 := by extra

[Heather Macbeth]

rzeta0 said:

my solution is so ugly!

I realise I'm only a beginner but I do feel such exercises don't teach anything about lean concepts, and are merely algebra torture with not much educational value.

@rzeta0 The "algebra torture" is probably necessary to discover a proof of this fact, but once you have done it in scratch work on paper, you don't need to write it out in Lean. See the shorter outline here for a hint.

[Heather Macbeth]

I would describe the "educational value" of this problem as follows: often in proof-based maths, you (i.e., the author) can invent a proof which is very short and easy for someone else to read and check, at the cost of doing a ton of work behind the scenes yourself.

This proof-writing style doesn't come naturally to most people: beginners tend to produce arguments like the ones in your initial post, which are easier to invent, but longer to read.

[Heather Macbeth]

Anyway, this indeed doesn't "teach anything about Lean concepts." Instead, it's a lesson about maths itself (and in fact Mechanics of Proof is really intended as a maths textbook, and only incidentally as a Lean textbook.)

[rzeta0]

Heather Macbeth said:

I would describe the "educational value" of this problem as follows: often in proof-based maths, you (i.e., the author) can invent a proof which is very short and easy for someone else to read and check, at the cost of doing a ton of work behind the scenes yourself.

Thank you - I had not considered this previously.