Inequalities with cast

Stream: new members

[Adomas Baliuka]

I proved a Real-number inequality where one of the inputs is a natural that is cast to Real. (The reason I do this is because an input of my function really should be Nat and participates in Real inequalities, I don't think it can be avoided. If anyone's interested, I'm using this for defining binary entropy in this PR )

Seemingly, this fact broke all the automation (or at least the way I usually use it). Is there some way to do this nicely?

import Mathlib

-- I also seem to have forgotten how to "multiply both sides of an inequality"
lemma aux {a b c : ℝ} (h : 0 < a) (hh : a * b < a * c) : b < c := by
  exact (mul_lt_mul_left h).mp hh

lemma inequality_with_conversion {q : ℕ} (qNot0 : 2 ≤ q) (x : ℝ)
  (hx : x < 1 - (↑q)⁻¹) :
    x < (q - 1) * (1 - x) := by
  have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qNot0
  have qnonz : (q : ℝ) ≠ 0 := by linarith
  have zero_le_qinv : 0 < (q : ℝ)⁻¹ := by positivity
  have : (q : ℝ)⁻¹ ≠ 0 := inv_ne_zero qnonz
  rw [show ((q:ℝ) - 1) * (1 - x) = q - q*x - 1 + x by ring]
  simp only [lt_add_iff_pos_left, lt_neg_add_iff_add_lt, add_zero]
  apply aux zero_le_qinv
  rw [mul_zero]
  have : (q:ℝ)⁻¹ * ((q:ℝ) - (q:ℝ) * x - 1) = 1 - x - (q:ℝ)⁻¹ := by
    calc (q:ℝ)⁻¹ * ((q:ℝ) - (q:ℝ) * x - 1)
      _ = (q:ℝ)⁻¹ * (q:ℝ) - (q:ℝ)⁻¹ * (q:ℝ) * x - (q:ℝ)⁻¹ := by ring
      _ = 1 - x - (q:ℝ)⁻¹ := by
        rw [inv_mul_cancel qnonz]
        simp only [one_mul]
  rw [this]
  linarith

[James Sundstrom]

Here's my attempt:

import Mathlib

lemma inequality_with_conversion {q : ℕ} (qNot0 : 2 ≤ q) (x : ℝ) (hx : x < 1 - (↑q)⁻¹) :
    x < (q - 1) * (1 - x) := by
  have qpos : (q : ℝ) > 0 := by positivity
  have : q * x < q - 1 := by
    convert (mul_lt_mul_left qpos).2 hx using 1
    simp [mul_sub, ne_of_gt qpos]
  linarith

[Adomas Baliuka]

Thanks, that's much nicer than what I did!

Any idea what might have been my error in thinking? Or things you can share about your thought process when you wrote the proof?

[Kevin Buzzard]

The thought process is: inverse is hard to work with (in the sense that all the big tactics like linarith and polyrith work with ring theory) so get rid of it ASAP by multiplying up, and then use a big tactic.