Proof that the |max f1 - max f2| <= max |f1 - f2|

Stream: new members

[Will Bradley]

image.png
To practice, I formalized this proof that the absolute difference in the maxima of two real-valued functions on a finite, non-empty set is not greater than the maximum absolute difference between them. (Note that the WLOG inequality assumption at the end of the second line should be reversed in the informal proof.) What can I improve, especially with regards to using Classical?

I wish I knew a way to both let-assign a variable from an Exists.choose and introduce a hypothesis that the variable satisfies the proposition of the Exists, like in choose_spec, but all in one step. In other words, I wish I could obtain x₁ with hx₁ and x₂ with hx₂ in one tactic or term-expression each.

import Mathlib.Data.Real.Basic
import Mathlib.Data.Set.Finite.Lemmas

attribute [local instance] Classical.propDecidable in
noncomputable def Set.liftFun {α: Type u} {β: Sort v} [Nonempty β] (X: Set α) (f: X → β): α → β :=
  fun x =>
    if hx: x ∈ X then
      f ⟨x, hx⟩
    else
      Classical.arbitrary β

structure FiniteNonemptySet (α: Type u) where
  set: Set α
  h₁: set.Finite
  h₂: set.Nonempty

namespace FiniteNonemptySet

variable (X: FiniteNonemptySet α) (f: X.set → ℝ)

theorem exists_argmax: ∃ x, ∀ y, f y ≤ f x := by
  obtain ⟨x, hx_mem, hx_max⟩ := X.set.exists_max_image (X.set.liftFun f) X.h₁ X.h₂
  exists ⟨x, hx_mem⟩
  intro ⟨y, hy_mem⟩
  have := hx_max y hy_mem
  simp [Set.liftFun, hx_mem, hy_mem] at this
  assumption

noncomputable def maxBy :=
  f (exists_argmax X f).choose

theorem absolute_difference_of_maxima_le_maximum_absolute_distance (f₁ f₂: X.set → ℝ): |X.maxBy f₁ - X.maxBy f₂| ≤ X.maxBy (fun x => |f₁ x - f₂ x|)
:= by
  wlog h : X.maxBy f₁ ≥ X.maxBy f₂
  · rw [abs_sub_comm]
    conv in (fun _ => _) =>
      intro
      rw [abs_sub_comm]
    apply this
    exact le_of_not_ge h
  · let x₁ := (X.exists_argmax f₁).choose
    have hx₁ := (X.exists_argmax f₁).choose_spec
    let x₂ := (X.exists_argmax f₂).choose
    have hx₂ := (X.exists_argmax f₂).choose_spec
    calc |X.maxBy f₁ - X.maxBy f₂|
      _ = X.maxBy f₁ - X.maxBy f₂ := by rwa [abs_eq_self, sub_nonneg]
      --_ = f₁ x₁ - f₂ x₂ := rfl
      _ ≤ f₁ x₁ - f₂ x₁ := tsub_le_tsub (hx₁ x₁) (hx₂ x₁)
      _ ≤ |f₁ x₁ - f₂ x₁| := le_abs_self _
      _ ≤ X.maxBy (fun x => |f₁ x - f₂ x|) := by
        simp [maxBy, -Subtype.forall]
        apply (X.exists_argmax (fun x => |f₁ x - f₂ x|)).choose_spec
end FiniteNonemptySet

[Aaron Liu]

let ⟨x, hx⟩ := Classical.indefiniteDescription _ ⋯

[Will Bradley]

@Aaron Liu Thank you! I was somehow just looking at that without connecting it to what I wanted

[Aaron Liu]

I have found this version to be harder to work with, due to both the higher-order unification problems it introduces (although that problem exists with Classical.choose and Classical.choose_spec too) and just that it is longer to type, and gives terms with match Classical.indefiniteDescription _ _ with | .mk x hx => ... in it.

[Will Bradley]

Actually, @Aaron Liu, the hypothesis given by indefiniteDescription for x₁ is different (x₁ ∈ X.set) than the one I have using choose_spec (∀ (y : ↑X.set), f₁ y ≤ f₁ ⋯.choose)

[Will Bradley]

And x₁ is definitionally equal to that ⋯.choose, I believe, so that's why it works

[Aaron Liu]

Not x₁, but the (exists_argmax X f).choose in the definition of maxBy

[Kevin Buzzard]

In this particular case you don't need to use choice at all; there is a better proof. To prove max|f-g|>=|max f - max g| it suffices to prove max|f-g| >= max f - max g and >= max g - max f, and by symmetry we only need to prove the first one. Rearranging, we need to prove max|f-g| + max g >= max f, but to prove something is >= max f, we only need to prove it's >= f(t) for all t (note that we're not using choice here, we're proving something for all t, not a special t) and this is obvious because max|f-g| >= |f(t)-g(t)| and max(g) >= g(t) by definition of max, and now the inequality follows from |f(t)-g(t)| >= f(t) - g(t).

[Will Bradley]

@Kevin Buzzard I'll try that, was following my written proof line-for-line. How do I even define the max of a finite, nonempty set constructively though?

[Aaron Liu]

You can use docs#Finset.max' or if you don't want to carry around proofs of nonempty then docs#Finset.max

[Will Bradley]

But @Aaron Liu I need the type parameter of the set to be a LinearOrder for that

[Aaron Liu]

What does the maximum mean if you don't have a linear order?

[Edward van de Meent]

you can try using the supremum instead?

[Edward van de Meent]

i.e., the maximum is the supremum of two comparable values

[Edward van de Meent]

in mathlib, i think this is what max or ⊔ refers to

[Aaron Liu]

That would be docs#Finset.sup, which works in a docs#SemilatticeSup with docs#OrderBot, and if you don't have a bottom element, then docs#Finset.sup' (but you need nonempty).

[Will Bradley]

Oh yeah lol. Sorry I forgot what my original goal was