NNReal subtraction is 2-Lipschitz

Stream: Is there code for X?

[Kalle Kytölä]

Here is a small puzzle-game for those who enjoy playing with NNReal. Maybe I'm missing something, but I would enjoy if this was less of a puzzle. What can we do? (For the record, I agree that subtraction in NNReal is pathological, but its 2-Lipschitzness is not pathological.)

Claim: Subtraction in ℝ≥0 (i.e., the mapping ℝ≥0 × ℝ≥0 → ℝ≥0 given by (x, y) ↦ x - y) is 2-Lipschitz.

Proof: The metric on the product ℝ≥0 × ℝ≥0 is the max-distance of the two components, so the claim is obvious. $\square$

import Mathlib.Data.Real.NNReal
import Mathlib.Tactic

open scoped NNReal

lemma NNReal.lipschitzWith_sub : LipschitzWith 2 (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2) := by
  sorry

Below is my Lean-attempt at the puzzle, but please try it first and decide whether you like NNReals, if you haven't already. (And then please golf my stupid solution.)

import Mathlib.Data.Real.NNReal
import Mathlib.Tactic

open scoped NNReal

lemma NNReal.lipschitzWith_sub_right (a : ℝ≥0) : LipschitzWith 1 (fun x ↦ (a - x).val) := by
  change LipschitzWith 1
    ((((fun (p : ℝ × ℝ) ↦ max p.fst p.snd) ∘ fun x ↦ (x, 0)) ∘ (fun x ↦ a + x) ∘ Neg.neg)
      ∘ (fun (x : ℝ≥0) ↦ x.val))
  have isom := (((isometry_add_left (a : ℝ)).comp isometry_neg).comp
                (@isometry_subtype_coe ℝ _ {x | 0 ≤ x}))
  simpa using ((lipschitzWith_max.comp (LipschitzWith.prod_mk_right 0))).comp isom.lipschitz

lemma NNReal.lipschitzWith_sub_left (a : ℝ≥0) : LipschitzWith 1 (fun x ↦ x - a) := by
  change LipschitzWith 1
    ((((fun (p : ℝ × ℝ) ↦ max p.fst p.snd) ∘ fun x ↦ (x, 0)) ∘ (fun x ↦ x - a))
      ∘ (fun (x : ℝ≥0) ↦ x.val))
  have isom := (isometry_add_right (-a : ℝ)).comp (@isometry_subtype_coe ℝ _ {x | 0 ≤ x})
  simpa using ((lipschitzWith_max.comp (LipschitzWith.prod_mk_right 0))).comp isom.lipschitz

lemma NNReal.lipschitzWith_sub : LipschitzWith 2 (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2) := by
  rw [lipschitzWith_iff_dist_le_mul]
  intro p q
  simp [ge_iff_le, NNReal.coe_ofNat]
  change dist (p.1 - p.2) (q.1 - q.2) ≤ 2 * (max (dist p.1 q.1) (dist p.2 q.2))
  simp only [ge_iff_le, dist_eq, two_mul]
  apply le_trans _ (add_le_add (le_max_left _ _) (le_max_right _ _))
  apply (abs_sub_le (p.1 - p.2).val (q.1 - p.2).val (q.1 - q.2).val).trans
  apply add_le_add
  · have aux := NNReal.lipschitzWith_sub_left p.2
    rw [lipschitzWith_iff_dist_le_mul] at aux
    simpa [dist_eq] using aux p.1 q.1
  · have aux := NNReal.lipschitzWith_sub_right q.1
    rw [lipschitzWith_iff_dist_le_mul] at aux
    simpa [dist_eq] using aux p.2 q.2

[Anatole Dedecker]

Okay I have a fun solution

[Anatole Dedecker]

This looks really annoying until you realize the existence of docs#LipschitzWith.max_const

[Anatole Dedecker]

import Mathlib.Data.Real.NNReal
import Mathlib.Tactic

open scoped NNReal

lemma Isometry.lipschitzWith_iff {α β γ : Type*} [PseudoEMetricSpace α] [PseudoEMetricSpace β]
    [PseudoEMetricSpace γ] {f : α → β} {g : β → γ} (K : ℝ≥0) (h : Isometry g) :
    LipschitzWith K f ↔ LipschitzWith K (g ∘ f) := by
  simp [LipschitzWith, h.edist_eq]

lemma NNReal.lipschitzWith_sub : LipschitzWith 2 (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2) := by
  rw [isometry_subtype_coe.lipschitzWith_iff]
  have : Isometry (Prod.map ((↑) : ℝ≥0 → ℝ) ((↑) : ℝ≥0 → ℝ)) :=
    isometry_subtype_coe.prod_map isometry_subtype_coe
  convert (((LipschitzWith.prod_fst.comp this.lipschitz).sub
    (LipschitzWith.prod_snd.comp this.lipschitz)).max_const 0)
  norm_num

[Anatole Dedecker]

(The first lemma should just be in the library)

[Anatole Dedecker]

Oh actually you were using lipschitzWith_max already

[Anatole Dedecker]

(Note that the proof is taking about 1s so probably we want to optimize it a bit before PR-ing)

[Eric Wieser]

lemma NNReal.lipschitzWith_sub : LipschitzWith 2 (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2) := by
  simp_rw [lipschitzWith_iff_dist_le_mul, Prod.dist_eq, NNReal.dist_eq, NNReal.coe_sub_def, NNReal.coe_two, two_mul]
  rintro ⟨x1, y1⟩ ⟨x2, y2⟩
  dsimp only
  refine (abs_max_sub_max_le_abs _ _ _).trans ?_
  rw [sub_sub_sub_comm]
  exact (abs_sub _ _).trans (add_le_add (le_max_left _ _) (le_max_right _ _))

is my solution

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

I think I prefer my solution since it doesn't involve unfolding the definition of LipschitzWith, but essentially we're doing the same thing.

[Kalle Kytölä]

I really adore Anatole's principled way of using only lemmas that should absolutely be expected to be there. And adding the one that wasn't! (...and as Anatole noted, the one thing that required knowing something specific in the library wass the existence of LipschitzWith.max_const.)

That said, Eric's solution essentially follows the elementary argument I had in mind in my pen-and-paper proof (Pf.: Obvious. $\square$), and Eric manages to do this 5 times more efficiently than I did!

Thank you both very much!

I'm trying figure out the lessons I (and maybe others) should learn, particularly for working with NNReal.

Anatole's solution is just a great reminder to stick to the clear, soft, and elegant mathematical reasoning. (It's not the first time I try to learn that, but I will try to learn it again --- in principle I know it pays off in formalization and in the real world.) This lesson seems more general than just a strategy to fight NNReals.

I really admire the efficiency of Eric's solution, but the general lesson from it seems less clear to me... Ok, unfolding the definition of NNReal subtraction early on was definitely a good idea, and finding the lemma abs_max_sub_max_le_abs was really helpful. I feel like I tried to do very similar things with less success...

[Kalle Kytölä]

Btw, I think lemmas of this flavor should go to Mathlib so that no one else ever has to do the puzzle again. :speechless:

Is the right statement to PR the 2-Lipschitzness of subtraction, or is there a more helpful one? Is there a good generalization that applies not only to NNReal?

[Eric Wieser]

I feel like I got lucky that my proof worked; once I unfolded to real, my strategy was just "guess lemmas names about max, sub, and abs until I find one that matches". Surprisingly I didn't hit any dead ends, but I find that I rarely get away with that strategy on inequalities

[Kalle Kytölä]

Indeed, it is worth noting that everyone got out of NNReal to Real more or less as fast as possible (except Anatole only did that on the codomain side in the first step and on the domain side a bit later...). Sure, this is reasonable --- especially if one knows or expects the Real API to be better.

[Anatole Dedecker]

An interesting thing about my solution is that (without even thinking about it) I basically mimicked the proof of docs#NNReal.instContinuousSubNNRealInstTopologicalSpaceNNRealInstSubNNReal

[Anatole Dedecker]

I guess this is the kind of proofs you get good at by combining tons of continuity/measurability/differentiability lemmas in similar ways

[Kalle Kytölä]

To me Lipschitzness seemed quantitative and continuity/measurability/differentiability seem qualitative... But you showed that the strategy worked with Lipschitzness, too!

(EDIT: maybe differentiability is not qualitative if you actually keep track of the differentials, as you often do!)

[Anatole Dedecker]

I never really used the Lipschitz API, so I was happily surprised about that too!

[Kalle Kytölä]

Anyways, for the PRs. I would personally like to see also the "partial results" (which are in fact quantitatively stronger than the general result) NNReal.lipschitzWith_sub_right and NNReal.lipschitzWith_sub_left in the library. But is there a generalization beyond NNReal?

[Kalle Kytölä]

And incidentally, the partial results in Real are not in Mathlib as far as I can see. But Reals are useless for puzzles:

lemma Real.lipschitzWith_sub_right (a : ℝ) : LipschitzWith 1 (fun x ↦ a - x) :=
  ((isometry_add_left a).comp isometry_neg).lipschitz

lemma Real.lipschitzWith_sub_left (a : ℝ) : LipschitzWith 1 (fun x ↦ x - a) :=
  (isometry_add_right (-a)).lipschitz

[Eric Wieser]

Kalle Kytölä said:

Indeed, it is worth noting that everyone got out of NNReal to Real more or less as fast as possible (except Anatole only did that on the codomain side in the first step and on the domain side a bit later...). Sure, this is reasonable --- especially if one knows or expects the Real API to be better.

I don't think this is an argument for avoiding NNReal; I think rather it's a case for avoiding subtraction in the junk zone if you can (i.e. by using docs#LipschitzOnWith in the valid region)

[Kalle Kytölä]

I agree --- and these types of results are about setting up the API, so the implementation isn't important at all (it is ok to go to Real fast). What matters is that once the API is there, the user doesn't face too challenging puzzles.