Proving sharp inequalities using interval arithmetic

Stream: metaprogramming / tactics

[Geoffrey Irving]

Per previous threads, I have an interval tactic in https://github.com/girving/interval/blob/main/Interval/Tactic/Interval.lean that works for constant inequalities. Can we push it to parameterized inequalities?

Here is a true claim, from https://arxiv.org/abs/2211.11731. @Yaël Dillies pointed me to this a while ago. Code from https://github.com/girving/interval/blob/main/Interval/Tactic/Frankl.lean:

import Interval.Tactic.Interval

/-!
# The inequality from Alweiss et al.
-/

open Real (log sqrt)
open Set
noncomputable section

def φ : ℝ := (sqrt 5 - 1) / 2

def H (x : ℝ) : ℝ := -x * log x - (1 - x) * log (1 - x)

lemma phi_pos : 0 < φ := by
  simp only [φ]
  interval

lemma alweiss_somewhere : 0.9 * H 0.9 ≤ φ * H (0.9 ^ 2) := by
  simp only [φ, H]
  interval

/-- It would be nice if `interval` did this -/
proof_wanted alweiss : ∀ x ∈ Icc φ 1, x * H x ≤ φ * H (x ^ 2)

Unfortunately, the inequality is sharp at 0 and 1; the difference plot looks like

difference.png

I think this means that the lowest-thought-required interval arithmetic strategy would be to

1. Use non-interval methods to prove the inequality at 0 and 1.
2. Use interval methods on the derivatives to show the inequality holds near the endpoints. Though unfortunately we need second derivatives on the left point, and on the right endpoint the derivative is -inf. :/
3. Use straightforward interval bisection on the interior.

But I'm not sure how to most easily organize the code for this. My constant-only interval tactic depends on a lifting function from real expressions to Interval expressions:

partial def lift (e : Q(ℝ)) : MetaM Q(Interval) := do
  match e with
    | ~q(0) => return q(0)
    | ~q(1) => return q(1)
    | ~q(@OfNat.ofNat ℝ $n $i) => return q(Interval.ofNat $n)
    | ~q(@OfNat.ofNat ℝ $n $i / @OfNat.ofNat ℝ $d $j) => return q(Interval.ofRat ($n / $d))
    | ~q(1 / @OfNat.ofNat ℝ $d $j) => return q(Interval.ofRat (1 / $d))
    | ~q(@OfScientific.ofScientific ℝ _ $x $u $t) => do
      return q(@OfScientific.ofScientific Interval _ $x $u $t)
    | ~q(-$x) => return q(-$(← lift x))
    | ~q($x + $y) => return q($(← lift x) + $(← lift y))
    | ~q($x - $y) => return q($(← lift x) - $(← lift y))
    | ~q($x * $y) => return q($(← lift x) * $(← lift y))
    | ~q($x / $y) => return q($(← lift x) / $(← lift y))
    | ~q(@HPow.hPow ℝ ℝ ℝ $i $x $y) => return q($(← lift x).pow $(← lift y))
    | ~q(Real.exp $x) => return q($(← lift x).exp)
    | ~q(Real.log $x) => return q($(← lift x).log)
    | ~q(|$x|) => return q($(← lift x).abs)
    | _ => throwError f!"`interval` works only for certain constant real inequalities, not {e}"

Naively if I want to adaptively deal with derivatives and singularities and such I'd have to change the lift to produce an intermediate expression language, write automatic differentiation on that expression language, etc., etc. It seems like a bunch of work.

Is there a clean, general way to go about this? In particular, is it possible to

1. Assume my interval tactic can handle expressions like ∀ x ∈ Icc a b, f x < g x as long as f, g are continuous and "well separated" (so that a decently fine subdivision of Icc a b cause the interval arithmetic to go through).
2. Write wrapper logic to handle the more general situation with precise endpoints and derivatives?

[Yaël Dillies]

Is the condition in 1. something like "g - f has small oscillation"?

[Geoffrey Irving]

More like “the interval extension F - G is nonnegative on a not too tiny subdivision, say 1000 subintervals”. This can fail for other reasons, “1e9 * x - 1e9 * x + 1” won’t have a nice interval extension, since the interval extensions won’t know the x’s are the same.

[Jihoon Hyun]

We can decide ∀ x ∈ Ioo a b, f x ≤ g x if the statement is false. I don't think there will be a program or tactic which decides ∀ x ∈ Ioo a b, f x < g x or ∀ x ∈ Icc a b, f x < g x without additional hypothesis.