Space of katetov maps + mathlib access

Stream: mathlib4

[Luigi Massacci]

I defined the space of Katetov maps on a metric space and related instances, and I think it's worth trying to PR it : ) Could I have mathlib access? My github is luigi-massacci

here is the content if anyone wants to give some comments in the meantime.

Definition and FunLike mumbo-jumbo:

import Mathlib.Tactic
import Mathlib.Topology.Compactification.OnePoint
import Mathlib.Data.Real.Archimedean
import Mathlib.Algebra.Order.Pointwise
import Mathlib.Topology.Separation
import Mathlib.Topology.MetricSpace.PseudoMetric

variable {X : Type _} [MetricSpace X]

structure IsKatetov (f : X → ℝ) : Prop where
  /-- Proposition that `f` is 1-Lipschitz -/
  abs_sub_le_dist : ∀ x y, |f x - f y| ≤ dist x y
  /-- Second defining inequality of a Katetov map  -/
  dist_le_add : ∀ x y, dist x y ≤ f x + f y

theorem IsKatetov_def {_ : MetricSpace X} {f : X → ℝ} :
    IsKatetov f ↔ (∀ x y, |f x - f y| ≤ dist x y) ∧ (∀ x y, dist x y ≤ f x + f y) :=
  ⟨fun h ↦ ⟨h.abs_sub_le_dist, h.dist_le_add⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

structure KatetovMap (X : Type*) [MetricSpace X] where
  /-- The function `X → ℝ` -/
  protected toFun : X → ℝ
  /-- Proposition that `toFun` is a Katetov map -/
  protected IsKatetovtoFun : IsKatetov toFun

notation "E(" X ")" => KatetovMap X

section

class KatetovMapClass (F : Type*) (X : Type*) [MetricSpace X] [FunLike F X  ℝ] where
  map_katetov (f : F) : IsKatetov f

end

export KatetovMapClass (map_katetov)

section KatetovMapClass

variable {F X : Type*} [MetricSpace X] [FunLike F X  ℝ]
variable [KatetovMapClass F X]

@[coe] def toKatetovMap (f : F) : E(X) := ⟨f, map_katetov f⟩

instance : CoeTC F E(X) := ⟨toKatetovMap⟩

end KatetovMapClass

namespace KatetovMap

variable {X : Type*} [MetricSpace X]

instance funLike : FunLike E(X) X ℝ where
  coe := KatetovMap.toFun
  coe_injective' f g h := by cases f; cases g; congr

instance toKatetovMapClass : KatetovMapClass E(X) X where
  map_katetov := KatetovMap.IsKatetovtoFun

@[simp]
theorem toFun_eq_coe {f : E(X)} : f.toFun = (f : X → ℝ) := rfl

instance : CanLift (X → ℝ) E(X) DFunLike.coe IsKatetov := ⟨fun f hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩

def Simps.apply (f : E(X)) : X → ℝ := f

initialize_simps_projections KatetovMap (toFun → apply)

@[simp]
protected theorem coe_coe {F : Type*} [FunLike F X ℝ] [KatetovMapClass F X] (f : F) :
    ⇑(f : E(X)) = f := rfl

@[ext]
theorem ext {f g : E(X)} (h : ∀ a, f a = g a) : f = g := DFunLike.ext _ _ h

protected def copy (f : E(X)) (f' : X → ℝ) (h : f' = f) : E(X) where
  toFun := f'
  IsKatetovtoFun := h.symm ▸ f.IsKatetovtoFun

@[simp]
theorem coe_copy (f : E(X)) (f' : X → ℝ) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

theorem copy_eq (f : E(X)) (f' : X → ℝ) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

variable {f g : E(X)}

theorem katetov_set_coe (s : Set E(X)) (f : s) : IsKatetov (f : X → ℝ) :=
  f.1.IsKatetovtoFun

theorem coe_injective : @Function.Injective E(X) (X → ℝ) (↑) :=
  fun f g h ↦ by cases f; cases g; congr

@[simp]
theorem coe_mk (f : X → ℝ) (h : IsKatetov f) : ⇑(⟨f, h⟩ : E(X)) = f :=
  rfl

end KatetovMap

MetricSpace and CompleteSpace instances:

lemma abs_sub_dist_le (x₀ : α) (f : E(α)) (x : α) : |f x - dist x x₀| ≤ f x₀ := by
  refine abs_le.mpr ⟨?_, ?_⟩
  · linarith [(map_katetov f).dist_le_add x x₀]
  · linarith [le_of_abs_le <| (map_katetov f).abs_sub_le_dist x x₀]

theorem bounded_dist_set {f g : E(α)} : BddAbove {|f x - g x| | x : α} := by
  by_cases hn : Nonempty α
  · have x₀ := Classical.choice ‹Nonempty α›
    refine ⟨f x₀ + g x₀, fun _ ⟨x, hx⟩ ↦ ?_⟩; rw [← hx]
    have h : |f x - g x| ≤ |f x - dist x x₀| + |g x - dist x x₀|:= by
      rw [← abs_sub_comm (dist x x₀) (g x)]; apply abs_sub_le (f x) (dist x x₀) (g x)
    apply le_trans h <| add_le_add (abs_sub_dist_le x₀ f x) (abs_sub_dist_le x₀ g x)
  · refine ⟨0, fun _ ⟨x, _⟩ ↦ False.elim (hn ⟨x⟩)⟩

lemma eq_zero_of_sSup_eq_zero (s : Set ℝ) (hb : BddAbove s) (snonneg : ∀ x ∈ s, 0 ≤ x)
    (hsup : sSup s = 0) : ∀ x ∈ s, x = 0 := by
  refine (fun x xs ↦ le_antisymm (by rw [← hsup]; exact le_csSup hb xs) (snonneg x xs))

theorem katetov_nonneg (f : E(α)) (x : α) : 0 ≤ f x := by
  have : 0 ≤ f x + f x := by rw [← dist_self x]; exact (map_katetov f).dist_le_add x x
  apply nonneg_add_self_iff.mp this

theorem empty_sSup_of_empty (h : IsEmpty α) (f g : E(α)) :
    ¬Set.Nonempty {|f x - g x| | x : α} := by
  by_contra hc
  obtain ⟨_, x, _⟩ := hc
  exact IsEmpty.false x

noncomputable instance: MetricSpace E(α) where
  dist f g := sSup {|f x - g x| | x : α}
  dist_self f := by
    by_cases h : Nonempty α
    · simp [dist]
    · simp [dist, sSup]
      have hf := empty_sSup_of_empty (not_nonempty_iff.mp h) f f
      simp only [sub_self, abs_zero] at hf
      simp_all only [false_and, dite_false, IsEmpty.forall_iff]
  dist_comm f g := by simp [dist, abs_sub_comm]
  dist_triangle f g h := by
    by_cases hc : Nonempty α
    · simp [dist]
      apply Real.sSup_le
      · rintro val ⟨x, rfl⟩
        rw [← csSup_add]
        · apply le_trans <| abs_sub_le (f x) (g x) (h x)
          apply le_csSup (by apply BddAbove.add <;> apply bounded_dist_set)
          refine Set.mem_add.mpr ⟨|f x - g x|, (by simp), (by simp)⟩
        · have x₀ := Classical.choice ‹Nonempty α›
          use |f x₀ - g x₀| ; simp
        · apply bounded_dist_set
        · have x₀ := Classical.choice ‹Nonempty α›
          use |g x₀ - h x₀| ; simp
        · apply bounded_dist_set
      · apply add_nonneg <;>
        { apply Real.sSup_nonneg; rintro val ⟨x, rfl⟩; apply abs_nonneg}
    · simp [dist, sSup]
      have hfh := empty_sSup_of_empty (not_nonempty_iff.mp hc) f h
      have hfg := empty_sSup_of_empty (not_nonempty_iff.mp hc) f g
      have hgh:= empty_sSup_of_empty (not_nonempty_iff.mp hc) g h
      simp_all only [false_and, dite_false]
      simp only [add_zero, le_refl]
  eq_of_dist_eq_zero := by
    intro f g h
    simp [dist] at h
    apply eq_zero_of_sSup_eq_zero at h
    · ext x; exact eq_of_sub_eq_zero <| abs_eq_zero.mp (h |f x - g x| ⟨x, rfl⟩)
    · apply bounded_dist_set
    · rintro _ ⟨x, rfl⟩; exact abs_nonneg _
  edist_dist x y:= by exact ENNReal.coe_nnreal_eq _

theorem dist_coe_le_dist (f g : E(α)) (x : α) : dist (f x) (g x) ≤ dist f g :=
  by refine le_csSup bounded_dist_set (by simp [dist])

theorem dist_le {C :ℝ} (C0 : (0 : ℝ) ≤ C) (f g : E(α)):
  dist f g ≤ C ↔ ∀ x : α, dist (f x) (g x) ≤ C := by
  refine ⟨fun h x => le_trans (dist_coe_le_dist _ _ x) h, fun H ↦ ?_⟩
  simp [dist]; apply Real.sSup_le (by simp [*] at *; assumption) (C0)

noncomputable instance : CompleteSpace E(α) :=
  Metric.complete_of_cauchySeq_tendsto fun (u : ℕ → E(α)) (hf : CauchySeq u) => by
    rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩
    have u_bdd := fun x n m N hn hm => le_trans (dist_coe_le_dist _ _ x) (b_bound n m N hn hm)
    have ux_cau : ∀ x, CauchySeq fun n => u n x :=
      fun x => cauchySeq_iff_le_tendsto_0.2 ⟨b, b0, u_bdd x, b_lim⟩
    choose f hf using fun x => cauchySeq_tendsto_of_complete (ux_cau x)
    have fF_bdd : ∀ x N, dist (u N x) (f x) ≤ b N :=
      fun x N => le_of_tendsto (tendsto_const_nhds.dist (hf x))
        (Filter.eventually_atTop.2 ⟨N, fun n hn => u_bdd x N n N (le_refl N) hn⟩)
    have kat_f : IsKatetov f := by
      have h : ∀ x y,∀ ε > 0, |f x - f y| ≤ 2*ε + dist x y ∧ dist x y ≤ f x + f y + 2*ε:= by
        intro x y ε εpos
        rcases Metric.tendsto_atTop.mp (hf x) ε εpos with ⟨Nx, hNx⟩
        rcases Metric.tendsto_atTop.mp (hf y) ε εpos with ⟨Ny, hNy⟩
        simp [dist] at *
        set N := max Nx Ny
        specialize hNx N (le_max_left _ _)
        specialize hNy N (le_max_right _ _)
        constructor
        · calc
          _ = _ := by rw [← add_zero (f x), (show 0 = u N x - u N x + u N y - u N y by ring)]
          _ = |(f x - (u N) x) + ((u N) y - f y) + ((u N x) - (u N y))|     := by ring_nf
          _ ≤ |(f x - (u N) x)| + |((u N) y - f y)| + |((u N x) - (u N y))| := by
              repeat apply (abs_add ..).trans; gcongr; try exact abs_add _ _
          _ ≤ 2*ε + dist x y := by
              rw [abs_sub_comm (f x)]
              linarith [(map_katetov (u N)).abs_sub_le_dist x y]
        · calc
          _ ≤ u N x + u N y := (map_katetov (u N)).dist_le_add x y
          _ = _ := by rw [← add_zero (u N y), show 0 = f x - f x + f y - f y by ring]
          _ = f x + f y + (u N x - f x) + (u N y - f y) := by ring
          _ ≤ _ := by linarith [le_of_lt (lt_of_abs_lt hNx), le_of_lt (lt_of_abs_lt hNy)]
      constructor <;>
        { refine fun x y ↦ le_of_forall_pos_le_add (fun ε εpos ↦ ?_)
          linarith [h x y (ε/2) (half_pos εpos)]}
    · use ⟨f, kat_f⟩
      refine' tendsto_iff_dist_tendsto_zero.2 (sq

[Patrick Massot]

Could you tell us a bit where this notion appears? It seems pretty arcane to me.

[Patrick Massot]

In the definition, why don’t you using our theory of Lipschitz map? This would probably save you a lot of work down the road.

[Patrick Massot]

I don’t know whether we currently have a way to autogenerate the first theorem but clearly you can use the same proof for both implications: fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩.

[Patrick Massot]

The metric space instance could very probably reuse existing things from Mathlib.

[Patrick Massot]

and same for completeness

[Luigi Massacci]

Yes of course. In reverse order:

• I'm sure there are, I just didn't find them. Especially for handling sSup I think there must be, but it was never quite right
• That was dumb of me I didn't even notice. As for autogeneration, I saw explicit instances were provided in a bunch of places (including Lipschitz) and just went along for the sake of conformity.
• It made life more complicated because of all the multiplications by 1. Might be a problem of defective user though

[Luigi Massacci]

As for their use, it's a very practical way to construct this and similar objects, and talk about them, and in the perspective of doing continuous logic in lean, they are useful for the continuous analogue of the Fraisse Theorem

[Riccardo Brasca]

It seems you already have access

[Luigi Massacci]

and here is the rest since I surpassed the character limit of Zulip:

namespace KatetovKuratowskiEmbedding

def instKatetovMapOfEmpty [IsEmpty α] : E(α) := by
  refine ⟨fun x ↦ (IsEmpty.false x).elim, ?_⟩
  constructor <;> {intro x; exact (IsEmpty.false x).elim}

theorem exists_isometric_embedding (α : Type*) [MetricSpace α] : ∃ f : α → E(α), Isometry f := by
    by_cases h : Nonempty α
    · refine ⟨fun x : α ↦ ⟨fun y ↦ dist x y, ?_⟩, ?_⟩
      · constructor <;> (intro y z; rw [dist_comm x y])
        · rw [dist_comm x z]; exact abs_dist_sub_le y z x
        · exact dist_triangle y x z
      · refine Isometry.of_dist_eq (fun x y ↦ le_antisymm ?_ ?_)
        · refine Real.sSup_le ?_ dist_nonneg
          · simp only [Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff]
            refine fun z ↦ abs_dist_sub_le x y z
        · refine (Real.le_sSup_iff bounded_dist_set ?_).mpr  ?_
          · have x₀ := Classical.choice ‹Nonempty α›
            use |dist x x₀ - dist y x₀| ; simp
          · simp only [KatetovMap.coe_mk, Set.mem_setOf_eq, exists_exists_eq_and]
            refine fun ε εpos ↦ ⟨x, ?_⟩
            rw [dist_self, zero_sub, abs_neg, dist_comm, abs_of_nonneg (dist_nonneg)]
            exact add_lt_of_neg_right (dist y x) εpos
    · refine ⟨fun _ ↦ @instKatetovMapOfEmpty _ _ (not_nonempty_iff.mp h), fun x ↦ ?_⟩
      exact ((not_nonempty_iff.mp h).false x).elim

end KatetovKuratowskiEmbedding

open KatetovKuratowskiEmbedding

noncomputable def katetovKuratowskiEmbedding (α : Type*) [MetricSpace α] : α ↪ E(α) := by
  choose f h using exists_isometric_embedding α; refine ⟨f, h.injective⟩

protected theorem katetovKuratowskiEmbedding.isometry (α : Type*) [MetricSpace α] :
  Isometry (katetovKuratowskiEmbedding α) :=
    Classical.choose_spec <| exists_isometric_embedding α

[Yaël Dillies]

You can generate IsKatetov_def by tagging IsKatetov with mk_iff