Optimizing proof |inf f - inf g| < sup |f - g|

Stream: new members

[Luigi Massacci]

Two questions:
a) Is this already in Mathlib somewhere? I couldn't find it in a reasonably close form.
b) If not, can it be shortened significantly? I would imagine all the "nonempty whatever" can be optmized.
c) If not, should the answer to a) become "yes"?

import Mathlib.Tactic
import Mathlib.Algebra.Order.Pointwise
import Mathlib.Data.Set.Image
import Mathlib.Data.Set.Pointwise.Basic
open Pointwise

lemma abs_inf_dist_le_sup {α : Type*} {f g : α → ℝ} (hα : Nonempty α)
 (fpos : ∀ x, 0 ≤ f x) (gpos : ∀ x, 0 ≤ g x) (hb : BddAbove (Set.range |f - g|)):
    |sInf {f x | x} - sInf {g x | x}| ≤ sSup {|f x - g x| | x} := by
    refine abs_le.mpr ⟨?_, ?_⟩
    · have : sInf {g x | x} - sSup {|f x - g x| | x} ≤ sInf {f x | x} := by
        rw [← csInf_sub _ _ _ (by exact hb)]
        · apply le_csInf
          · have z₀ := Classical.choice hα
            refine ⟨f z₀, by simp⟩
          · rintro _ ⟨x, rfl⟩
            refine @csInf_le_of_le _ _ ({x | ∃ x_1, g x_1 = x} - {x | ∃ x_1, |f x_1 - g x_1| = x})
              (f x) (g x - |f x - g x|) ?_ ?_ ?_
            · simp_rw [sub_eq_add_neg]
              apply BddBelow.add ?_ (BddAbove.neg hb)
              · refine ⟨0, ?_⟩;rintro _ ⟨x, rfl⟩; apply gpos
            · apply Set.mem_sub.mpr
              refine ⟨g x, (by simp), |f x - g x|, by simp, by ring⟩
            · nth_rewrite 1 [← abs_of_nonneg (gpos x), abs_sub_comm _ _]
              calc
              _ ≤ |g x - (g x - f x)| := by exact abs_sub_abs_le_abs_sub (g x) _
              _ = f x := by ring_nf; rw [abs_of_nonneg (fpos x)]
        · have z₀ := Classical.choice hα
          refine ⟨g z₀, by simp⟩
        · refine ⟨0, ?_⟩; rintro _ ⟨x, rfl⟩; apply gpos
        · have z₀ := Classical.choice hα
          refine ⟨|f z₀ - g z₀|, by simp⟩
      linarith [this]
    · have : sInf {f x | x} - sSup {|f x - g x| | x} ≤ sInf {g x | x} := by
        rw [← csInf_sub _ _ _ (by exact hb)]
        · apply le_csInf
          · have z₀ := Classical.choice hα
            refine ⟨g z₀, by simp⟩
          · rintro _ ⟨x, rfl⟩
            refine @csInf_le_of_le _ _ ({x | ∃ x_1, f x_1 = x} - {x | ∃ x_1, |f x_1 - g x_1| = x})
              (g x) (f x - |f x - g x|) ?_ ?_ ?_
            · simp_rw [sub_eq_add_neg]
              apply BddBelow.add ?_ (BddAbove.neg hb)
              · refine ⟨0, ?_⟩; rintro _ ⟨x, rfl⟩; apply fpos
            · apply Set.mem_sub.mpr ⟨f x, (by simp), |f x - g x|, by simp, by ring⟩
            · nth_rewrite 1 [← abs_of_nonneg (fpos x)]
              calc
              _ ≤ |f x - (f x - g x)| := by exact abs_sub_abs_le_abs_sub (f x) _
              _ = g x := by ring_nf; rw [abs_of_nonneg (gpos x)]
        · have z₀ := Classical.choice hα
          refine ⟨f z₀, by simp⟩
        · refine ⟨0, ?_⟩; rintro _ ⟨x, rfl⟩; apply fpos
        · have z₀ := Classical.choice hα
          refine ⟨|f z₀ - g z₀|, by simp⟩
      linarith [this]

[Eric Wieser]

Note that sSup { f x | x } is usually better written as iSup f (or with the notation for that function)

[Luigi Massacci]

I am bumping this up again, since I didn't get anywhere. I did rewrite the statement of the theorem in terms of iSup and iInf since it was convenient when applying it, but proof wise I don't see a series of rewrites that is as simple as the one above (so I ended up rewriting iSupand iInf to csSup and csInf on the first line and kept everything else the same). I did cut the length of the proof in half by adding a separate lemma:

import Mathlib

open Pointwise

lemma inf_sub_sup_le_inf {α : Type*} {f g : α → ℝ}
 (fpos : ∀ x, 0 ≤ f x) (gpos : ∀ x, 0 ≤ g x) (hb : BddAbove (Set.range |f - g|)):
    iInf g - iSup |f - g| ≤ iInf f := by
  by_cases hα : Nonempty α
  · rw [iInf, iSup, ← csInf_sub ⟨g (Classical.choice hα), by simp⟩ _ _ (by exact hb)]
    · apply le_csInf ⟨f (Classical.choice hα), by simp⟩
      rintro _ ⟨x, rfl⟩
      refine @csInf_le_of_le _ _ ({g x | x} - {|f x - g x| | x})
        (f x) (g x - |f x - g x|) ?_ ⟨g x, (by simp), |f x - g x|, by simp, by ring⟩ ?_
      · simp_rw [sub_eq_add_neg]
        apply BddBelow.add ?_ (BddAbove.neg hb)
        · refine ⟨0, ?_⟩;rintro _ ⟨x, rfl⟩; apply gpos
      · nth_rewrite 1 [← abs_of_nonneg (gpos x), abs_sub_comm _ _]
        calc
        _ ≤ |g x - (g x - f x)| := by exact abs_sub_abs_le_abs_sub (g x) _
        _ = f x := by ring_nf; rw [abs_of_nonneg (fpos x)]
    · refine ⟨0, ?_⟩; rintro _ ⟨x, rfl⟩; apply gpos
    · have z₀ := Classical.choice hα
      refine ⟨|f z₀ - g z₀|, by simp⟩
  · simp [not_nonempty_iff.mp hα]

lemma abs_sub_inf_le_sup {α : Type*} {f g : α → ℝ}
 (fpos : ∀ x, 0 ≤ f x) (gpos : ∀ x, 0 ≤ g x) (hb : BddAbove (Set.range |f - g|)):
    |iInf f - iInf g| ≤ iSup |f - g| := by
    refine abs_le.mpr ⟨?_, ?_⟩
    · linarith [inf_sub_sup_le_inf fpos gpos hb]
    · rw [abs_sub_comm] at *
      linarith [inf_sub_sup_le_inf gpos fpos hb]

[Eric Wieser]

One obvious thing from your proof is that BddBelow.sub is missing; that would a be nice thing to PR (along with the BddAbove version)

[Luigi Massacci]

Good point

[Eric Wieser]

Here's how I'd clean things up a bit:

import Mathlib

open Pointwise

set_option autoImplicit false
variable {α β : Type*}

lemma bddBelow_range (f : α → β) [Preorder β] : BddBelow (Set.range f) ↔ ∃ b, ∀ x, b ≤ f x := by
  simp [BddBelow, Set.Nonempty, mem_lowerBounds]

lemma BddBelow.range {f : α → β} [Preorder β] (b : β) (hf : ∀ x, b ≤ f x) : BddBelow (Set.range f) :=
  bddBelow_range _ |>.mpr ⟨_, hf⟩

lemma BddBelow.sub {s t : Set α} [Preorder α] [AddGroup α]
    [CovariantClass α α (· + ·) (· ≤ ·)]
    [CovariantClass α α (Function.swap (· + ·)) (· ≤ ·)]
    (hs : BddBelow s) (ht : BddAbove t) : BddBelow (s - t) := by
  simpa [sub_eq_add_neg] using hs.add ht.neg

lemma inf_sub_sup_le_inf {α : Type*} {f g : α → ℝ}
    (fpos : ∀ x, 0 ≤ f x) (gpos : ∀ x, 0 ≤ g x) (hb : BddAbove (Set.range |f - g|)):
    iInf g - iSup |f - g| ≤ iInf f := by
  cases isEmpty_or_nonempty α
  · simp
  rw [iInf, iSup, ← csInf_sub (Set.range_nonempty _) _ _ hb]
  · refine le_ciInf fun x => ?_
    refine csInf_le_of_le (b := g x - |f x - g x|) ?_ ?_ ?_
    · exact .sub (.range _ gpos) hb
    · exact Set.sub_mem_sub (Set.mem_range_self _) (Set.mem_range_self _)
    · nth_rewrite 1 [← abs_of_nonneg (gpos x), abs_sub_comm _ _]
      calc
        _ ≤ |g x - (g x - f x)| := abs_sub_abs_le_abs_sub (g x) _
        _ = f x := by ring_nf; rw [abs_of_nonneg (fpos x)]
  · exact .range _ gpos
  · exact Set.range_nonempty _

[Eric Wieser]

rintro _ ⟨x, rfl⟩ is a great tool, but to get shorter proofs, you should avoid it until you're sure that there isn't already a useful lemma

[Eric Wieser]

In this case, you missed out on Set.range_nonempty and Set.mem_range_self

[Anatole Dedecker]

What about this?

import Mathlib.Tactic
import Mathlib.Algebra.Order.Pointwise
import Mathlib.Data.Set.Image
import Mathlib.Data.Set.Pointwise.Basic
open Pointwise

lemma abs_inf_dist_le_sup {α : Type*} {f g : α → ℝ} (hα : Nonempty α)
    (fpos : ∀ x, 0 ≤ f x) (gpos : ∀ x, 0 ≤ g x) (hb : BddAbove (Set.range |f - g|)):
    |(⨅ x, f x) - (⨅ x, g x)| ≤ ⨆ x, |f x - g x| := by
  set C := ⨆ x, |f x - g x|
  have hC : ∀ x, |f x - g x| ≤ C := le_ciSup hb
  simp_rw [abs_sub_le_iff, forall_and, sub_le_iff_le_add] at hC ⊢
  suffices ∀ (u v : α → ℝ), 0 ≤ u → 0 ≤ v →
      (∀ x, u x ≤ C + v x) → (⨅ x, u x) ≤ C + (⨅ x, v x) from
    ⟨this f g fpos gpos hC.1, this g f gpos fpos hC.2⟩
  intro u v upos vpos hC
  rw [add_ciInf ⟨0, Set.forall_mem_range.mpr vpos⟩]
  refine ciInf_mono ⟨0, Set.forall_mem_range.mpr upos⟩ hC

[Anatole Dedecker]

Note that it gets even simpler if you assume directly that f and g are bounded below x)

[Luigi Massacci]

Thanks to the both of you