Coarse notions on metric spaces: Review+Help

Stream: new members

[bottine]

I've started trying to write down this quasi-isometry stuff that I want to attack. The first step, I thought, is probably to write down some properties of metric spaces. I've hit some roadblocks, and thought it could be useful to get some feedback.
Here is the code:

import data.int.interval
import topology.algebra.ordered.compact
import topology.metric_space.emetric_space


universes u

open filter function set fintype function emetric_space
open_locale nnreal ennreal


section space

  variables (α : Type u) [pseudo_emetric_space α]

  def is_locally_finite :=
    ∀ x : α, ∀ r : ℝ≥0, (emetric.ball x r).finite

  def is_uniformly_locally_finite_with (k : ℝ≥0 → ℕ) :=
    is_locally_finite α ∧ ∀ x : α, ∀ r : ℝ≥0,  ((emetric.ball x r).to_finset).card ≤ (k r)

  def is_uniformly_locally_finite :=
    ∃ k : ℝ≥0 → ℕ, is_uniformly_locally_finite_with α k

  def is_coarsely_connected_with (K : ℝ≥0) :=
    ∀ x x' : α,
      ∃ n : ℕ, ∃ w : fin (n+1) → α,
        w (fin.mk 0 (nat.zero_lt_succ n)) = x ∧
        w  (fin.mk n (by simp))= x' ∧   -- not sure how to make that clean
        ∀ (i j : fin n), edist (w i) (w j) ≤ K * | j-i |

  def is_coarsely_geodesic_with (K k : ℝ≥0) :=
    ∀ x x' : α,
      ∃ n : ℕ, ∃ w : fin (n+1) → α,
        w (fin.mk 0 (nat.zero_lt_succ n)) = x ∧
        w  (fin.mk n (by simp))= x' ∧   -- lol
        ∀ (i j : fin n), edist (w i) (w j) ≤ K * | j-i | ∧ (| j-i | : ℝ≥0∞) ≤ k * (edist (w i) (w j))

end space

section subset

variables {α : Type u} [pseudo_emetric_space α]

  def is_coarsely_dense_in_with (ε : ℝ≥0) (s t : set α) :=
    ∀ ⦃x⦄ (hx : x ∈ t), ∃ ⦃y⦄ (hy : y ∈ s), edist x y ≤ ε

  def is_coarsely_dense_with (ε : ℝ≥0) (s : set α) :=
    is_coarsely_dense_in_with ε s s-- (set.univ α) TODO !!! replace s by set.univ α in such a way that it typechecks

  def is_coarsely_dense_in (s t : set α)  :=
    ∃ (ε : ℝ≥0) , is_coarsely_dense_in_with ε s t

  def is_coarsely_dense (s : set α)  :=
    ∃ (ε : ℝ≥0) , is_coarsely_dense_with ε s

  def is_net (s : set α) := is_coarsely_dense s

  def is_coarsely_separated_with  (δ : ℝ≥0) (s : set α)  :=
    ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), x ≠ y → edist x y > δ
  -- We take > δ to get a better "duality" between coarsely separated and dense

  def is_coarsely_separated  (s : set α) :=
    ∃ δ : ℝ≥0 , δ > 0 ∧  is_coarsely_separated_with δ s
  -- We need to assume δ>0 because δ=0 would just imply that s (with induced metric) is an emetric space
  -- rather than a pseudo-emetric space

  def is_coarsely_separated_net_in_with  (δ ε : ℝ≥0) (s t : set α) :=
    is_coarsely_separated_with δ s ∧ is_coarsely_dense_in_with ε s t

  def is_coarsely_separated_net_with  (δ ε : ℝ≥0) (s : set α) :=
    is_coarsely_separated_with δ s ∧ is_coarsely_dense_with ε s

  def is_coarsely_separated_net_in (s t : set α) :=
    (is_coarsely_separated s) ∧ (is_coarsely_dense_in s t)

  def is_coarsely_separated_net (s : set α) :=
    (is_coarsely_separated s) ∧ (is_coarsely_dense s)



  -- Facts related to density
  namespace is_coarsely_dense_in_with

    lemma refl (s : set α) :
      is_coarsely_dense_in_with 0 s s
    := begin
      rintros x xs,
      use x,
      split,
      { exact xs,},
      { simp,}
    end

    lemma trans {ε ε' : ℝ≥0} {r s t : set α} :
      is_coarsely_dense_in_with ε r s →  is_coarsely_dense_in_with ε' s t →
      is_coarsely_dense_in_with (ε + ε') r t
    := begin
      rintros r_in_s s_in_t,
      rintros z zt,
      rcases s_in_t zt with ⟨y,ys,yd⟩ ,
      rcases r_in_s ys with ⟨x,xr,xd⟩,
      use x,
      split,
      { exact xr, },
      {
        calc edist z x ≤ (edist z y) + (edist y x) : edist_triangle z y x
                   ... ≤ ε           + ε'        : sorry --  by linarith [xd,yd] -- sorry -- best way here?
      }
    end

    lemma weaken {ε ε' : ℝ≥0} {s s' t t' : set α } :
      is_coarsely_dense_in_with ε s t →  s ⊆ s' →  t' ⊆ t →  ε ≤ ε' →
      is_coarsely_dense_in_with ε' s' t'
    := begin
      intros s_in_t s_sub_s' t'_sub_t ε_le_ε' ,
      rintros z zt',
      have zt : z ∈ t, from t'_sub_t zt',
      cases s_in_t zt with x xgood,
      cases xgood with xs xd,
      have xs' : x ∈ s', from s_sub_s' xs,
      use x,
      split,
      { exact xs'},
      {
        calc edist z x ≤ ε  : xd
                   ... ≤ ε' : ennreal.coe_le_coe.mpr ε_le_ε',
      },


    end

  end is_coarsely_dense_in_with

  namespace coarsely_separated_net

    def is_max_coarsely_separated_in_with (δ : ℝ≥0) (s S : set α) :=
      s ⊆ S ∧
      is_coarsely_separated_with δ s  ∧
      (∀ t : set α, s ⊆ t → t ⊆ S →  is_coarsely_separated_with δ t → s = t)


    lemma max_coarsely_separated_in_is_net (δ : ℝ≥0) (s S: set α) :
      is_max_coarsely_separated_in_with δ s S → is_coarsely_separated_net_in_with δ δ s S
    := begin
      rintros ⟨s_sub_S, s_sep, s_max⟩,
      split,
      { exact s_sep},
      {
        rintros x xS,
        let t := s.insert x,
        by_contradiction H,
        push_neg at H,
        have x_notin_s : x ∉ s, {
          by_contradiction x_in_s,
          -- and then?
          have lol : edist x x > δ, from H x_in_s,
          sorry, -- and then?

        }, -- use h telling us that x is far from all elements of s
        have s_sub_t : s ⊆ t , from subset_insert x s,
        have s_ne_t : s ≠ t , from ne_insert_of_not_mem s x_notin_s,
        have t_sub_S : t ⊆ S, from insert_subset.mpr ⟨xS, s_sub_S⟩,
        have : is_coarsely_separated_with δ t,
        {
          rintros x xt,
          rintros y yt,

          -- apply forall_insert_of_forall,
          -- actually need set.forall_insert_of_forall
          sorry,
        },
        exact s_ne_t (s_max t s_sub_t t_sub_S this),
      }
    end

    lemma exists_max_coarsely_separated_in_with (δ : ℝ≥0) (S : set α) :
      ∃ s : set α, is_max_coarsely_separated_in_with δ s S
    := begin
      sorry -- Zorn
    end

    lemma exists_coarsely_separated_net_in_with (δ : ℝ≥0) (S : set α) :
      ∃ s ⊆ S, is_coarsely_separated_net_in_with δ δ s S
    := begin
      rcases exists_max_coarsely_separated_in_with δ S with ⟨s, s_sub_S, s_sep, s_max_sep⟩,
      use s,
      split,
      { exact s_sub_S },
      { exact max_coarsely_separated_in_is_net δ s S ⟨s_sub_S, s_sep, s_max_sep⟩ },
    end
  end coarsely_separated_net

end subset

There are a few sorrys that I'd be glad to get help on. Also, since I'd eventually like to have it merged, any more consequent critics/discussion would be welcome. I can also describe my further plans!

[Johan Commelin]

I don't know anything about metric spaces. But I do know that mathlib heavily relies on filters, and I expect that a bunch of these concepts that you are defining would have to be connected to the filter library so that these developments play well together.

Also, since I'd eventually like to have it merged, any more consequent critics/discussion would be welcome.

Minor stylistic issue: we don't indent declarations inside sections/namespaces. So the word def or lemma always appears flush left. (There are some very old files in mathlib that don't do this. We should fix that.)

[bottine]

Minor stylistic issue: we don't indent declarations inside sections/namespaces. So the word def or lemma always appears flush left. (There are some very old files in mathlib that don't do this. We should fix that.) Noted!

[bottine]

Concerning filters, I'm not really sure: As far as I know/see it, these coarse notions on metric spaces don't have much topological content to them… but maybe I'm misled here

[Johan Commelin]

You should also prove all the different implications between these notions. And take advantage of dot-notation in the names.
If you prove is_foo → is_bar, then call the lemma is_foo.is_bar. Because then you can use it as follows: if you have an assumption h : is_foo somewhere, and you want is_bar, you can simply write h.is_bar.

[bottine]

Should trivial implications also be proved? As in, if I define a property extending another one, the "weakening" deserves a lemma? Similarly, I don't know how many variations on a definition should be provided (say being dense relative to instead of just being dense, or the _with versions, etc). In a sense, I feel like it can be a waste to define every single minor variation and implication, if I don't know that I will use them.

[Johan Commelin]

bottine said:

Should trivial implications also be proved? As in, if I define a property extending another one, the "weakening" deserves a lemma?

Library users will thank you if you do that for them.

[Johan Commelin]

If you look at things like continuous you will see that there are variations continuous_at, continuous_within and same for deriv etc... And systematic ways of passing from one to the other. It takes a bit of effort to set this up, but afterwards it is pleasant to use.

[Patrick Massot]

There are some things that make sense for any topological spaces in this. There are also many things that make sense in any uniform space but I'm not sure this is worth the trouble. I will help you clean this but I don't have time right now. Please make sure you follow the style guide and repost your code.

[Daniel Roca González]

The right generality are not uniform spaces, but coarse spaces.
Coarse structures (like the ones induces by metric spaces) are "dual" to uniform spaces: this measn that rather than being filters thet are "cofilters", so to speak. One can go about it by defining them via the "cocoarse filter" instead: in the metric case, these are the set of subsets of X times X whose complements have bounded diameter. I actually defined that a while ago if you think it's good to take that approach.

[Daniel Roca González]

import order.filter.lift
import topology.subset_properties
import topology.uniform_space.basic
import topology.metric_space.basic
import data.real.nnreal
import tactic.rewrite_search.frontend

open set filter topological_space

open_locale uniformity topological_space big_operators filter nnreal ennreal

set_option eqn_compiler.zeta true

universes u
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ι : Sort*}

def coid_rel {α : Type*} := {p : α × α | p.1 ≠ p.2}

@[simp] theorem nmem_coid_rel {a b : α} : (a, b) ∈ @coid_rel α ↔ a ≠ b := iff.rfl

@[simp] theorem coid_rel_subset {s : set (α × α)} : s ⊆ coid_rel ↔ ∀ a, (a, a) ∉ s :=
by simp [subset_def]; exact forall_congr (λ a, by
begin
  split,
  show (∀ (b : α), (a, b) ∈ s → ¬a = b) → (a, a) ∉ s,
  by {contrapose, simp,},
  show (a, a) ∉ s → (∀ (b : α), (a, b) ∈ s → ¬a = b),
  by {
    intros not_diag b in_s,
    have := not_diag,
    by_contradiction,
    rw ←h at in_s,
    contradiction,
  }
end)

@[simp] theorem co_of_coid_id_rel : (@coid_rel α)ᶜ = id_rel :=
begin
  ext v,
  unfold coid_rel id_rel,
  simp,
end

/-- The composition of corelations -/
def cocomp_rel {α : Type u} (r₁ r₂ : set (α×α)) := {p : α × α | ∀z:α, (p.1, z) ∈ r₁ ∨ (z, p.2) ∈ r₂}

localized "infix ` □ `:55 := cocomp_rel" in coarse

@[simp] theorem mem_cocomp_rel {r₁ r₂ : set (α×α)}
  {x y : α} : (x, y) ∈ r₁ □ r₂ ↔ ∀ z, (x, z) ∈ r₁ ∨ (z, y) ∈ r₂ := iff.rfl

@[simp] theorem not_mem_cocomp_rel {r₁ r₂ : set (α×α)}
  {x y : α} : (x, y) ∉ r₁ □ r₂ ↔ ∃ z, (x, z) ∉ r₁ ∧ (z, y) ∉ r₂ :=
begin
  split,
  {
    intro not_in_comp,
    simp at not_in_comp,
    cases not_in_comp with z g,
    by_contra h,
    simp at h,
    have either_r : (x, z) ∈ r₁ ∨ (z, y) ∈ r₂,
    {
      exact or_iff_not_imp_left.mpr (h z),
    },
    contradiction,
  },
  {
    intro exists_in_neither,
    cases exists_in_neither with z hz,
    simp,
    use z,
    exact not_or_distrib.mpr hz,
  }
end

@[simp] lemma co_of_cocomp_eq_comp_of_co {r₁ r₂ : set(α×α)} :
  (r₁ □ r₂)ᶜ = r₁ᶜ ○ r₂ᶜ :=
begin
  ext v,
  cases v with x y,
  simp,
  push_neg,
  exact iff.rfl,
end

@[simp] lemma not_comp_iff_cocomp_of_co {r₁ r₂ : set(α×α)}
  : (r₁ ○ r₂)ᶜ = r₁ᶜ □ r₂ᶜ :=
begin
  apply compl_inj_iff.mp,
  simp,
  exact boolean_algebra.to_core (set (α × α)), -- why is this needed?
end

@[simp] theorem swap_coid_rel : prod.swap '' coid_rel = @coid_rel α :=
set.ext $ assume ⟨a, b⟩, by simp [image_swap_eq_preimage_swap]; rw eq_comm


theorem monotone_cocomp_rel [preorder β] {f g : β → set (α×α)}
  (hf : monotone f) (hg : monotone g) : monotone (λx, (f x) □ (g x)) :=
begin
  unfold monotone,
  intros a b lt,
  unfold cocomp_rel,
  simp,
  intros a' b' h z,
  cases h z,
  {
    left,
    apply hf lt,
    exact h_1,
  },
  {
    right,
    apply hg lt,
    exact h_1,
  }
end



@[mono]
lemma cocomp_rel_mono {f g h k: set (α×α)} (h₁ : h ⊆ f) (h₂ : k ⊆ g) : h □ k ⊆ f □ g  :=
begin
  unfold cocomp_rel, simp,
  intros a b h z,
  have := h z,
  tauto,
end


lemma prod_mk_nmem_cocomp_rel {a b c : α} {s t : set (α×α)} (h₁ : (a, c) ∉ s) (h₂ : (c, b) ∉ t) :
  (a, b) ∉ s □ t :=
begin
  simp,
  use c,
  push_neg,
  split,
  assumption',
end

@[simp] lemma coid_cocomp_rel {r : set (α×α)} : coid_rel □ r = r :=
begin
  apply compl_inj_iff.mp,
  rw co_of_cocomp_eq_comp_of_co,
  simp,
end

lemma cocomp_rel_assoc {r s t : set (α×α)} :
  (r □ s) □ t = r □ (s □ t) :=
begin
  apply compl_inj_iff.mp,
  repeat {rw co_of_cocomp_eq_comp_of_co},
  exact comp_rel_assoc,
end

lemma subset_cocomp_self {α : Type*} {s : set (α × α)} (h : s ⊆ coid_rel) : s □ s ⊆ s :=
λ ⟨x, y⟩ xy_in, by {
  simp at h,
  simp at xy_in,
  have := xy_in y,
  cases this,
  assumption,
  have := h y,
  contradiction,
}


structure coarse_space (α : Type u) :=
(cocoarse   : filter (α × α))
(corefl     : cocoarse ≤ 𝓟 coid_rel)
(symm       : tendsto prod.swap cocoarse cocoarse)
(cocomp       : cocoarse ≤ cocoarse.lift' (λs, s □ s))

def coarse_space.mk' {α : Type u} (U : filter (α × α))
  (corefl : coid_rel ∈ U)
  (symm : ∀ r ∈ U, prod.swap ⁻¹' r ∈ U)
  (cocomp : ∀ r ∈ U, r □ r ∈ U) : coarse_space α :=
⟨U, λ r ru, mem_of_superset corefl ru, symm,
  begin
    intros v h,
    rw [mem_lift'_sets] at h,
    rcases h with ⟨w, hw, hcomp⟩,
    have : w □ w ∈ U, by {exact cocomp w hw},
    apply mem_of_superset this, exact hcomp,
    refine monotone_cocomp_rel _ _, tidy,
  end⟩

lemma coarse_space.eq :
  ∀{u₁ u₂ : coarse_space α}, u₁.cocoarse = u₂.cocoarse → u₁ = u₂
| ⟨u₁, _, _, _⟩  ⟨u₂, _, _, _⟩ h := by { congr, exact h }

attribute [class] coarse_space


section coarse_space
variables [coarse_space α]

def cocoarse (α : Type u) [s : coarse_space α] : filter (α × α) :=
  @coarse_space.cocoarse α s

localized "notation `𝓒'` := cocoarse" in cocoarse

def coarse (α : Type u) [s : coarse_space α] : set (set (α×α)) :=
  compl '' (𝓒' α).sets

localized "notation `𝓒` := coarse" in cocoarse

lemma mem_coarse {s : set (α×α)} : s ∈ 𝓒 α ↔ sᶜ ∈ 𝓒' α :=
begin
  split,
  {rintro h, rcases h with ⟨t, h_h_left, rfl⟩, simpa,},
  {rintro h, use sᶜ, simpa,}
end

lemma cocoarse_le_corefl : 𝓒' α ≤ 𝓟 coid_rel :=
@coarse_space.corefl α _

lemma corefl_mem_cocoarse :
  coid_rel ∈ 𝓒' α :=
begin
  have := @coarse_space.corefl α _,
  simpa,
end

lemma mem_cocoarse_of_eq {x y : α} {s : set (α × α)} (hx : x ≠ y) :
  ∃ s ∈ 𝓒' α, (x, y) ∈ s :=
begin
  use coid_rel,
  split, by {exact corefl_mem_cocoarse},
  simpa,
end

lemma symm_le_cocoarse : map (@prod.swap α α) (𝓒' _) ≤ (𝓒' _) :=
(@coarse_space.symm α _)

lemma cocoarse_le_cocomp : 𝓒' α ≤ (𝓒' α).lift' (λs:set (α×α), s □ s) :=
(@coarse_space.cocomp α _)

lemma tendsto_swap_cocoarse : tendsto (@prod.swap α α) (𝓒' α) (𝓒' α) :=
symm_le_cocoarse

lemma cocomp_mem_cocoarse_sets {s : set (α × α)} (hs : s ∈ 𝓒' α) :
  s □ s ∈ 𝓒' α :=
begin
  apply cocoarse_le_cocomp,
  rw mem_lift'_sets, use s, split,
  {assumption},
  {intros x h, assumption,},
  {refine monotone_cocomp_rel _ _, tidy,}
end


end coarse_space


lemma mem_cocoarse_dist' [metric_space α] {s : set (α×α)} : s ∈ (⨅ r∈{r:ℝ|r≥0},  𝓟 ({p:α×α | dist p.1 p.2 ≤ r}ᶜ)) ↔ (∃ r≥0, ∀ {p:α×α}, p ∈ sᶜ → dist p.1 p.2 ≤ r) :=
begin
  rw mem_binfi_of_directed _ _,
  show directed_on ((λ (i : ℝ), 𝓟 {p : α × α | dist p.fst p.snd ≤ i}ᶜ) ⁻¹'o ge) {r : ℝ | r ≥ 0},
  by {
    intros r₁ h₁ r₂ h₂,
    use max r₁ r₂,
    simp, tauto,
  },
  show {r : ℝ | r ≥ 0}.nonempty,
  by {use 1, simp,},
  simp [subset_def],
  split,
  repeat {
    rintro ⟨r, _, h⟩, use r,
    split, assumption,
    intros a b, contrapose, simp, apply h,
  },
end



instance coarse_of_bounded_space [metric_space α] : coarse_space α :=
{ cocoarse := (⨅ r∈{r:ℝ|r≥0}, 𝓟 ({p:α×α | dist p.1 p.2 ≤ r}ᶜ)),
  corefl := by {
    have : (1 : ℝ) > (0 : ℝ),
    by linarith,
    have lm : 𝓟 ({p : α × α | dist p.fst p.snd ≤ 1}ᶜ) ≤ 𝓟 coid_rel,
    by {
      rw [principal_le_iff],
      intros V hV,
      rw mem_principal at hV,
      refine subset.trans _ hV,
      intro p, cases p with x y,
      simp only [not_le, mem_set_of_eq, nmem_coid_rel, ne.def, mem_compl_eq],
      intro v,
      have : dist x y ≠ 0,
      by linarith,
      rwa dist_ne_zero at this,
    },
    refine trans _ lm,
    rw filter.le_def,
    simp only [ mem_cocoarse_dist'],
    intros s h, use 1,
    simp only [true_and, zero_le_one, prod.forall, ge_iff_le, mem_compl_eq],
    simp [compl_subset_comm] at h,
    intros a b in_s,
    have := h in_s, simp at this, assumption,
  },
  symm := by {
    intros f hf,
    simp only [ge_iff_le, mem_map],
    simp only [mem_cocoarse_dist'] at *,
    simp at *,
    conv in (∃ (r : ℝ), 0 ≤ r ∧ ∀ (x y : α), (y, x) ∉ f → dist x y ≤ r)
    begin
      congr, funext,
      rw forall_swap,
      find (dist _ _) {rw dist_comm},
    end,
    tauto,
  },
  cocomp := by {
    intro s,
    rw filter.mem_lift'_sets,
    show monotone (λ (s : set (α × α)), s □ s), by {exact monotone_cocomp_rel monotone_id monotone_id},
    rintro ⟨t, ⟨h, cocomp_subset⟩⟩,
    have comp_subset : sᶜ ⊆ tᶜ ○ tᶜ, by {rw ←compl_subset_compl, simpa,},
    rw mem_cocoarse_dist' at *,
    rcases h with ⟨r, r_ge_0, t_has_diam⟩,
    use 2*r,
    have two_r_ge_0 : 2 * r ≥ 0, by linarith,
    refine ⟨two_r_ge_0, _⟩,
    rintro p in_compl_s,
    have := comp_subset in_compl_s,
    rcases this with ⟨z, xz_in_compl_t, zy_in_compl_t⟩,
    have : dist p.fst z ≤ r ∧ dist z p.snd ≤ r,
    by exact ⟨t_has_diam xz_in_compl_t, t_has_diam zy_in_compl_t⟩,
    have := dist_triangle p.1 z p.2,
    linarith,
  }
}

open_locale cocoarse

lemma mem_cocoarse_dist [metric_space α] {s : set (α×α)} : s ∈ 𝓒' α ↔ (∃ (r : ℝ) , r ≥ 0 ∧ ∀ {a b : α}, (a, b) ∈ sᶜ → dist a b ≤ r) :=
begin
  have unfold_prod : (∃ (r : ℝ) , 0 ≤ r ∧ ∀ {a b : α}, (a, b) ∈ sᶜ → dist a b ≤ r) = (∃ r≥0, ∀ {p:α×α}, p ∈ sᶜ → dist p.1 p.2 ≤ r),
  by simp,
  rw [unfold_prod, ←mem_cocoarse_dist'],
  tauto,
end


lemma mem_coarse_dist [metric_space α] {s : set (α×α)} : s ∈ 𝓒 α ↔ (∃ (r : ℝ) , r ≥ 0 ∧ ∀ {a b : α}, (a, b) ∈ s → dist a b ≤ r) :=
begin
  rw mem_coarse,
  rw mem_cocoarse_dist,
  simp,
end

theorem cocoarse_basis_dist [metric_space α] :
  (𝓒' α).has_basis (λ r : ℝ, r ≥ 0) (λ r, {p:α×α | dist p.1 p.2 > r}) :=
begin
  rw filter.has_basis_iff, intro t,
  rw mem_cocoarse_dist, split,
  {
    rintro ⟨r, compl_t_bounded_by_r⟩, use r,
    rw [←compl_subset_compl, subset_def],
    simpa,
  },
  {
    rintro ⟨r, r_ge_0, coball_subset_t⟩, use r,
    rw [←compl_subset_compl, subset_def] at coball_subset_t,
    simp [mem_compl_iff] at *,
    tauto,
  }
end

[bottine]

@Patrick Massot Great, thanks! Shall I repost here?

[bottine]

@Daniel Roca González Interesting… do you have literature on the subject? Also, Does this greater generality make my code redundant? how do you see both fitting together? I'm somewhat wary of "generality creep", and would rather have something basic up and running than chasing the best interface, though it's probably also better not to rush towards the first construction I stumble upon.

[bottine]

(I'd particularly appreciate literature on this duality with uniform spaces.)

[Kevin Buzzard]

@bottine is this work just for a project you're doing to learn Lean or are you thinking of ultimately PRing things to mathlib?

[bottine]

I'd hope to PR, eventually, if I manage to write PR-able code. This current code is a mix of learning the basics and trying to set up grounds for doing GGT.

[Patrick Massot]

I think we should try to prove a couple of things with both the low-tech version and the fancy version and see whether this makes any difference. If the fancy version is harder to use then we should definitely stick to the low-tech one. In the case of uniform spaces many metric proofs are actually easier in the fancy setup, because it gets rid of irrelevant stuff.

[Patrick Massot]

You should also make sure @Sebastien Gouezel is aware of your efforts. He formalized a lot of metric geometry in Isabelle (including Gromov hyperbolicity).

[Sebastien Gouezel]

Yes, I am subscribed to this thread :-)

[Rémi Bottinelli]

OK, I'm slowly cleaning up the space.lean, coarse_lipschitz.lean, coarse_antilipschitz.lean files here: https://github.com/bottine/mathlib/tree/quasi_isometry/src/topology/metric_space/coarse . The plan is to have everything needed to easily show the equivalence between the different definitions of quasi-isometries.

[Patrick Massot]

Did you read the style guide? It would help discussing interesting things if you could fix indentation, braces, dangling colon-equal etc.

[Daniel Roca González]

I've also been doing a skeleton for the abstract coarse space version and proven that metric spaces are coarse. (A "coarse space" is an abstract definition of a space with a notion of sets of bounded diameter).

[Rémi Bottinelli]

Patrick Massot said:

Did you read the style guide? It would help discussing interesting things if you could fix indentation, braces, dangling colon-equal etc.

I did. I meant to ping you once things are clean but to share my progress in the meantime. Sorry for the confusion!

[Daniel Roca González]

One way to talk about quasiisometries would be as follows: in general a coarse equivalence is not QI, but a coarse equivalence between geodesic spaces is, but most coarse spaces are coarse equivalent to a geodesic space, so we get QI equivalences for free. The problem is that the proof of this may be out of reach (we need topological versions of graphs).

[Daniel Roca González]

https://github.com/leanprover-community/mathlib/tree/coarse_structure_ggt/src/topology/coarse

[Rémi Bottinelli]

@Daniel Roca González Re. "a coarse equivalence between geodesic space is [QI]": If that is because the "coarse control functions" between your spaces are then necessarily affine, then I guess you don't need geodesicity, but just that any distance is realized by a "coarse walk", no?

[Daniel Roca González]

If by a "coarse walk" you mean a QI path from A to B, then yes I think so. If you mean a coarse map from A to B then maybe not.

[Rémi Bottinelli]

I mean that there exists some K>0 such that for any two points x,y in the space at distance d, there exists a sequence of something like d/K points each at distance at most K from their predecessor/successor, starting with x, and ending with y.

[Daniel Roca González]

Yes, I'm pretty sure that's the same as being QI to a geodesic space, not coarse equivalent.
A coarse map is a map which is proper and bornologous, which in a metric space means:

lemma metric.coarse_proper_iff (f : α → β) :
  coarse.proper f ↔ (∀ b : set β, emetric.diam b ≠ ⊤ → emetric.diam (f ⁻¹' b) ≠ ⊤) :=
sorry

lemma metric.bornologous_iff (f : α → β) : coarse.bornologous f
  ↔ (∀ (R : ℝ≥0), ∃ (S : ℝ≥0), ∀ x y, dist x y < R → dist (f x) (f y) < S) :=
sorry

[Daniel Roca González]

yeah, I think that would make things easier, you're right. I'll see if it's actually enough.

[Rémi Bottinelli]

Well, if the principal goal is GGT, then it's reasonable to work with the assumption that all spaces are coarsely geodesic/graphs/whatever, so I wouldn't reject the idea of dropping the pedestrian approach I tried.

[Daniel Roca González]

yes, that sounds good. I'll try to prove that being coarsely geodesic is enough.

[Daniel Roca González]

@Patrick Massot what do you think of the definition of coarsely geodesic in Rémis branch? Can it be simplified in some way? It's quite convoluted, but I can't see how to simplify it...
https://github.com/bottine/mathlib/blob/quasi_isometry/src/topology/metric_space/coarse/space.lean

[Rémi Bottinelli]

Re the definition I used: I think it would be cleaner to say that \alpha is coarsely geodesic if there exists (K,L,k,l) such that for any pair of points x y, there exists a (K,L,k,l) quasi-isometric embedding from a path graph to the space with end points x and y. This is closest to "coarsifying" the strict definition I guess.

[Rémi Bottinelli]

But I thought it might make more sense to have a definition without needing to define quasi-isometric embeddings first.

[Daniel Roca González]

No, I do think the definition should use QI embeddings

[Patrick Massot]

Rémi, you need to learn about

import data.fin.basic

variables n : ℕ

#check fin.last n

#check (0 : fin $ n+1)

[Rémi Bottinelli]

@Patrick Massot I tried to follow most of the guidelines wrt alignment: https://github.com/bottine/mathlib/blob/quasi_isometry/src/topology/metric_space/coarse/ (see only files spaces.lean, and coarse_(anti)lipschitz.lean, but haven't documented the code).

[Rémi Bottinelli]

If possible, I'd like some feedback on the following:

• The definition of is_uniformly_locally_finite_with doesn't type-check, and I'm not sure how to make it do: how do I tell .card that I really have a finset?
• Generally, how do I decide on having _with variants or not, and how do I deal with the doubling of code this entails?
• In max_coarsely_separated_in_is_net, I haven't yet managed to finish the proof, if someone wants to fill it in!
• Same for the exists_max_coarsely_separated_in_with.
• In files coarsely_(anti)lipschitz.lean, I have plenty of proofs by calculations that are relatively trivial, but filling in the steps is often tedious and results in long terms. Am I doing something wrong? It essentially all follows from monotonicity of all functions involved.
• How to cleanly deal with implicit arguments coherently?
• Similarly, is there a way to deal with coercion more efficiently than I do?

And then, I'll want to define quasi-isometric embeddings and quasi-isometries. I think I now have close to all lemmas necessary to show that all reasonable definitions are equivalent. Is there any preference of which definition to use?

To be honest, this code feels very messy, and I'm not sure how to make it properly organized.

[Patrick Massot]

For you first question, you can use:

variables (α : Type u) [pseudo_emetric_space α]

class is_locally_finite :=
(fintype_ball : ∀ x : α, ∀ r : ℝ≥0, fintype (ball x r))

attribute [instance] is_locally_finite.fintype_ball

def is_uniformly_locally_finite_with [is_locally_finite α] (k : ℝ≥0 → ℕ) :=
∀ x : α, ∀ r : ℝ≥0,  card (ball x r) ≤ k r


def is_uniformly_locally_finite [is_locally_finite α] :=
∃ k : ℝ≥0 → ℕ, is_uniformly_locally_finite_with α k

[Patrick Massot]

But really is_locally_finite is a strange name since your definition doesn't seem to be equivalent to local finiteness as a topological space.

[Patrick Massot]

The natural definition would have an existential quantifier on the radius, so that the definition says that every point has some finite neighborhood.

[Patrick Massot]

An easy solution if you insist on using this definition is to rename it finite_balls_space or something like this.

[Patrick Massot]

In topology the natural definition is

class loc_finite_space (α : Type u) [topological_space α] : Prop :=
(has_basis : ∀ x : α, (𝓝 x).has_basis (λ s : set α, s ∈ 𝓝 x ∧ finite s) id)

lemma loc_finite_space_of_bases {α : Type u} [topological_space α]
  {ι : Sort*} {p : ι → Prop} {s : α → ι → set α}
  (h : ∀ x, (𝓝 x).has_basis p (s x)) (h' : ∀ x i, p i → finite (s x i)) :
  loc_finite_space α :=
⟨begin
  intro x,
  apply (h x).to_has_basis,
  { intros i pi,
    exact ⟨s x i, ⟨(h x).mem_of_mem pi, h' x i pi⟩, by refl⟩ },
  { rintros U ⟨U_in, hU⟩,
    rcases (h x).mem_iff.mp U_in with ⟨i, pi, hi⟩,
    exact ⟨i, pi, hi⟩ }
end⟩

[Patrick Massot]

About _with variants, it really depends on whether you need this in math. There is no Lean-only answer.

[Patrick Massot]

I also did your missing proof:

    have : is_coarsely_separated_with δ t,
    { rintros z (rfl | zs) y (rfl | ys),
     { exact λ h, (h rfl).elim },
     { exact λ hzy, H ys },
     { intro hzy,
       rw edist_comm,
       exact H zs },
     { exact s_sep zs ys } },

[Patrick Massot]

I exhausted my time budget, I'll return to this later if nobody else beats me to it.

[Rémi Bottinelli]

Patrick Massot said:

But really is_locally_finite is a strange name since your definition doesn't seem to be equivalent to local finiteness as a topological space.

Indeed, I see now that the naming is not ideal. The problem is that in the case of arbitrary metric space, the definition of "finite balls" is not as clear as in the case of graphs, for which this is the same as "locally finite".

[Rémi Bottinelli]

And thanks for your time and the snippet :)

[Yaël Dillies]

Also, please stop taking common names in the root namespace :smile:
I swear I had no clue what docs#locally_finite was about before I went to see the docs.

[Daniel Roca González]

@Rémi Bottinelli for locally compact metric spaces (which are the ones we'll be interested in) your definition should be equal to the usual topological one: you can use compact sets instead of balls in the locally compact case

[Daniel Roca González]

docs#locally_finite is a genuinely different thing, since it's a property for families of sets, not of spaces.

[Yaël Dillies]

Yeah of course. I'm mentioning it for the name, not for the meaning.

[Yaël Dillies]

People would have probably been quite upset if I called docs#locally_finite_order locally_finite.

[Rémi Bottinelli]

Yaël Dillies said:

Also, please stop taking common names in the root namespace :smile:
I swear I had no clue what docs#locally_finite was about before I went to see the docs.

Mmh, is that an actual problem? I thought the folder hierarchy induced its own namespacing, making it OK

[Rémi Bottinelli]

@Daniel Roca González I'm not sure what you're aiming at. In "your definition should be", are you saying that whatever definition we take for "locally finite", we want it to agree with the topological definition ? I think this is already the case if the space is locally compact: any ball can be covered by finitely many balls of a given radius, hence is finite, so we're good. Are we?

[Alex J. Best]

The folder heierachy is more just for organising things, it has no effect on namespace.
The sort of issue we encounter is if you have a bunch of things imported because you are working on, say, manifolds which have a lot of prerequisites. We need to be able to write things unambiguously
For instance what should locally_finite G mean for some topogical group?
It could mean that G is locally finite as a topological space, or it could mean that G is locally finite as a group.
The way we solve this is with explicit namespaces in the code. So

namespace topological_space
def locally_finite ...
end topological_space

means that locally_finite defined there is really called topological_space.locally_finite if someone then wants to work on topology they open topological_space and then locally_finite refers only to that notion.

The folder structure has no effect on namespaces though

[Rémi Bottinelli]

Ah, I see, thanks for the explanation!

[Rémi Bottinelli]

But, say, I define "coarse lipschitz" maps at some point: coarse_lipschitz. I presume those fit in the root namespace because the name is pretty unambiguous, or should everything be namespaced, essentially?

[Daniel Roca González]

@Rémi Bottinelli yes, that's what I want to say: I don't think it should have a different name, because in all cases we're interested in it's equivalent

[Daniel Roca González]

rather, if we want to phrase it in a different way, we should use an iff lemma in the setting we want: see docs#metric.continuous_iff for an example of something like this

[Rémi Bottinelli]

And re namespaces: shall I just wrap it all in a namespace coarse … end coarse namespace? Does having this namespace mean I could/should drop the "coarse"/"coarsely" adjectives in my names?

[Yaël Dillies]

I personally prefer more descriptive names over namespaces.

[Rémi Bottinelli]

[o/t: I don't know if thumbsup is the proper "ack" emoji/reaction, or if it's interpreted here as approbation]

[Kevin Buzzard]

I usually use it to mean "I agree"

[Rémi Bottinelli]

ah, mmh, then maybe I shall use the octopus, whatever this one means :)

[Reid Barton]

The topology library got a pass on namespacing to some extent by being first (and by being important) but there are some names in it (like embedding maybe?) that should probably be namespaced

[Alex J. Best]

Rémi Bottinelli said:

ah, mmh, then maybe I shall use the octopus, whatever this one means :smile:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/octopus/near/199551941 :grinning: :octopus:

[Patrick Massot]

I'm back with a bit of time. I'm reading a bit more the space file. Note that mathlib's tradition is that stupid lemmas can have obfuscated proofs so you can write:

lemma refl (s : set α) : is_coarsely_dense_with_in 0 s s :=
λ x xs, ⟨x, xs, by simp⟩

[Patrick Massot]

Then the next proofs can be compressed without loosing any readability:

lemma trans {ε ε' : ℝ≥0} {r s t : set α}
  (r_in_s : is_coarsely_dense_with_in ε r s) (s_in_t : is_coarsely_dense_with_in ε' s t) :
  is_coarsely_dense_with_in (ε + ε') r t :=
begin
  rintros z zt,
  rcases s_in_t zt with ⟨y,ys,yd⟩ ,
  rcases r_in_s ys with ⟨x,xr,xd⟩,
  use [x, xr],
  calc edist z x ≤ edist z y + edist y x : edist_triangle z y x
                ... ≤ ε'          + ε    : add_le_add yd xd
                ... = ε + ε'             : add_comm _ _
end

lemma weaken {ε ε' : ℝ≥0} {s s' t t' : set α }
  (s_in_t : is_coarsely_dense_with_in ε s t)
  (s_sub_s' : s ⊆ s') (t'_sub_t : t' ⊆ t) (ε_le_ε' : ε ≤ ε') :
  is_coarsely_dense_with_in ε' s' t' :=
begin
  rintros z zt',
  have zt : z ∈ t, from t'_sub_t zt',
  rcases s_in_t zt with ⟨x, xs, xd⟩,
  have xs' : x ∈ s', from s_sub_s' xs,
  use [x, xs'],
  calc edist z x ≤ ε  : xd
             ... ≤ ε' : ennreal.coe_le_coe.mpr ε_le_ε'
end

[Patrick Massot]

If you want to rather improve readability then you can add type ascriptions and use obtain:

lemma weaken {ε ε' : ℝ≥0} {s s' t t' : set α }
  (s_in_t : is_coarsely_dense_with_in ε s t)
  (s_sub_s' : s ⊆ s') (t'_sub_t : t' ⊆ t) (ε_le_ε' : ε ≤ ε') :
  is_coarsely_dense_with_in ε' s' t' :=
begin
  rintros (z : α) (zt' : z ∈ t'),
  have zt : z ∈ t, from t'_sub_t zt',
  obtain ⟨x: α, xs : x ∈ s, xd : edist z x ≤ ε⟩ := s_in_t zt,
  have xs' : x ∈ s', from s_sub_s' xs,
  use [x, xs'],
  calc edist z x ≤ ε  : xd
             ... ≤ ε' : ennreal.coe_le_coe.mpr ε_le_ε'
end

[Patrick Massot]

Things like

  split,
  { exact s_sep},

in max_coarsely_separated_in_is_net costs one level of indent for very little gain. You can use refine ⟨s_sep, _⟩

[Patrick Massot]

The lines

  have x_notin_s : x ∉ s,
   { by_contradiction x_in_s,

prove that you are not quite yet used to how negation is handled in Lean. And I really with by_contradiction would refuse to do that. By definition, x ∉ s means x ∈ s → false. So your first line should be intro x_in_s.

[Patrick Massot]

The proof

lemma symm {K : ℝ≥0} {f₀ f₁ : α → β} :
  are_close_with K f₀ f₁ →  are_close_with K f₁ f₀ :=
begin
  intro acw,
  intro x,
  specialize acw x,
  rw ←edist_comm (f₀ x) (f₁ x),
  exact acw,
end

should be

lemma symm {K : ℝ≥0} {f₀ f₁ : α → β} :
  are_close_with K f₀ f₁ → are_close_with K f₁ f₀ :=
begin
  intros acw x,
  rw ← edist_comm,
  exact acw x,
end

[Patrick Massot]

For

lemma trans {K L : ℝ≥0} {f g h: α → β} (c : are_close_with K f g) (d : are_close_with L g h) :
  are_close_with (K + L) f h :=
begin
  intro x,
  let y := f x,
  let z := g x,
  let w := h x,
  calc edist y w ≤ edist y z + edist z w : edist_triangle _ _ _
              ... ≤ ↑K        + ↑L        : add_le_add (c x) (d x)
              ... = ↑(K + L)              : by simp,
end

it is enough and more readable to write

lemma trans {K L : ℝ≥0} {f g h: α → β} (c : are_close_with K f g) (d : are_close_with L g h) :
  are_close_with (K + L) f h :=
λ x, calc edist (f x) (h x) ≤ edist (f x) (g x) + edist (g x) (h x) : edist_triangle _ _ _
              ... ≤ K        + L        : add_le_add (c x) (d x)

[Patrick Massot]

Did you know that lambda can destructure stuff as in

lemma symm  (f₀ f₁ : α → β) : are_close f₀ f₁ →  (are_close f₁ f₀) :=
λ ⟨K₀,cw₀⟩, ⟨K₀,are_close_with.symm cw₀⟩

[Patrick Massot]

Beware it can't do the rfl magic of rintro

[Patrick Massot]

I hope you can learn stuff from some compression.

lemma close_composites_of_dense {ε : ℝ≥0} {s : set α} (cdw : is_coarsely_dense_with ε s) :
∃ retract : α → subtype s,
  are_close_with ε (coe ∘ retract) (@id α) ∧
  are_close_with ε (retract ∘ coe) (@id (subtype s)) :=
begin
    -- First we restate `cdw` in terms the axiom of choice likes:
  have cdw' : ∀ x : α, ∃ y : subtype s, edist x ↑y ≤ ε,
  { intro x,
    rcases cdw (mem_univ x) with ⟨y, ys, yd⟩,
    exact ⟨⟨y,ys⟩, yd⟩ },
  choose ret good using cdw',
  use ret,
  split ;
  { intros x,
    rw edist_comm,
    exact good x }
end

[Patrick Massot]

lemma range_of_coarse_identity {C : ℝ≥0} {f : α → α} (close : are_close_with C id f) :
  is_coarsely_dense_with C (range f) :=
λ x hx, ⟨f x, mem_range_self x, close x⟩

[Patrick Massot]

I'm moving to the coarse_lipschitz file. You should learn about docs#le_rfl which is a version of docs#le_refl with an implicit argument

[Patrick Massot]

lemma iff_range_restriction_is (K L: ℝ≥0) (f : α → β)  :
  coarse_lipschitz_with K L f ↔ coarse_lipschitz_with K L (range_factorization f) :=
begin
  split,
  { intro clw,
    intros x y,
    --rw range_factorization_coe,
    rw subtype.edist_eq _ _,
    rw range_factorization_coe,
    rw range_factorization_coe,
    apply clw,},
  { intro clw,
    intros x y,
    rw ←range_factorization_coe f x,
    rw ←range_factorization_coe f y,
    rw ←subtype.edist_eq _ _,
    apply clw,},
end

could be

lemma iff_range_restriction_is (K L: ℝ≥0) (f : α → β)  :
  coarse_lipschitz_with K L f ↔ coarse_lipschitz_with K L (range_factorization f) :=
by simp only [coarse_lipschitz_with, subtype.edist_eq, range_factorization_coe]

[Patrick Massot]

lemma of_coarse_lipschitz_images
  {K L : ℝ≥0} {f : α → β} (clf : coarse_lipschitz_with K L f)
  {ε : ℝ≥0} {s t : set α} (cdiw : is_coarsely_dense_with_in ε s t) :
  is_coarsely_dense_with_in (L + K*ε) (f '' s) (f '' t) :=
begin
  rintros _ ⟨x, xt, rfl⟩,
  rcases cdiw xt with ⟨y, ys, yd⟩,
  use [f y, mem_image_of_mem f ys],
  calc edist (f x) (f y) ≤ L + K * edist x y  : clf _ _
                        ... ≤ L + K * ε      : le_add_mul le_rfl le_rfl yd
                        ... ≤ (L + K * ε : ℝ≥0)      : by simp
end

[Patrick Massot]

lemma iff_range_restriction_is {f : α → β}  :
  coarse_lipschitz f ↔ coarse_lipschitz (range_factorization f) :=
⟨λ ⟨K, L, clwf⟩, ⟨K, L, (coarse_lipschitz_with.iff_range_restriction_is K L f).mp clwf⟩,
 λ ⟨K, L, clwf⟩, ⟨K, L, (coarse_lipschitz_with.iff_range_restriction_is K L f).mpr clwf⟩

[Patrick Massot]

I'm not sure what to say about painful computation. The main issue here is the classic issue that linarith doesn't handle nnreal and ennreal. But you can still simplify a bit as in

lemma comp
  {Kf Lf : ℝ≥0} {f : α → β} (clf : coarse_lipschitz_with Kf Lf f)
  {Kg Lg : ℝ≥0} {g : β → γ} (clg : coarse_lipschitz_with Kg Lg g) :
  coarse_lipschitz_with (Kg * Kf) (Lg + Kg * Lf) (g ∘ f) :=
λ x y, calc
edist ((g ∘ f) x)  ((g ∘ f) y) ≤ Lg + Kg * (edist (f x) (f y)) : clg (f x) (f y)
                           ... ≤ Lg + Kg * (Lf + Kf * edist x y) : le_add_mul le_rfl le_rfl (clf x y)
                           ... = (Lg + Kg * Lf ) + (Kg * Kf) * edist x y : by ring
                           ... = _ : by simp

[Rémi Bottinelli]

Woah, thanks a lot!

[Patrick Massot]

Note there is no mathematical content to all those modifications. I've blindly applied usual Lean tricks. I couldn't tell what this is all about, I didn't read any statement.

[Rémi Bottinelli]

I assume I should mostly read pieces of mathlib to get more of these tricks/literacy?

[Kevin Buzzard]

You should just keep writing code and then other people will look at it and tell you tricks. At least, that's what I did. I found mathlib impossible to read and very intimidating as a learner.

[Rémi Bottinelli]

Works for me :)

[Rémi Bottinelli]

Patrick Massot said:

lemma iff_range_restriction_is {f : α → β}  :
  coarse_lipschitz f ↔ coarse_lipschitz (range_factorization f) :=
⟨λ ⟨K, L, clwf⟩, ⟨K, L, (coarse_lipschitz_with.iff_range_restriction_is K L f).mp clwf⟩,
 λ ⟨K, L, clwf⟩, ⟨K, L, (coarse_lipschitz_with.iff_range_restriction_is K L f).mpr clwf⟩

Any reason this is not by simpa only [coarse_lipschitz_with.iff_range_restriction_is] beside variety for pedagogical purposes ?

[Rémi Bottinelli]

(I say simpa because simp doesn't seem to work)

[Kevin Buzzard]

I bet the longer proof compiles much quicker. It's swings and roundabouts probably (some advantages, some disadvantages). The longer proof doesn't fire up the tactic framework at all.

[Rémi Bottinelli]

I assume there is a kind of proof refinement process, where you start with "whatever you came up with that typechecks" and then refine the code until you get something striking a balance between readable, robust and efficient.

[Kevin Buzzard]

I think that when it comes to mathlib, robust is at the top of the list, and readable at the bottom (although not everyone likes the latter decision)

[Patrick Massot]

Rémi Bottinelli said:

I assume I should mostly read pieces of mathlib to get more of these tricks/literacy?

I hope you will already learn a lot by carefully comparing what you originally wrote with my version. This is much more efficient than reading efficient proofs that you didn't try to write yourself. This is precisely the reason why I did this yesterday.

[Patrick Massot]

Rémi Bottinelli said:

Patrick Massot said:

lemma iff_range_restriction_is {f : α → β}  :
  coarse_lipschitz f ↔ coarse_lipschitz (range_factorization f) :=
⟨λ ⟨K, L, clwf⟩, ⟨K, L, (coarse_lipschitz_with.iff_range_restriction_is K L f).mp clwf⟩,
 λ ⟨K, L, clwf⟩, ⟨K, L, (coarse_lipschitz_with.iff_range_restriction_is K L f).mpr clwf⟩

Any reason this is not by simpa only [coarse_lipschitz_with.iff_range_restriction_is] beside variety for pedagogical purposes ?

No, in that case I simply noticed your proof wasn't a real tactic proof (no rw or simp) so it could be turned into a proof term. And also the proof sounded like something you wouldn't bother mentioning on paper so it was eligible for obfuscation.

[Kevin Buzzard]

I am constantly doing this (golfing code) with students too -- they show me some code and I reply with some code which is much more compressed and often does the same thing in the same way. It's miserable having to write 40 lines doing something which looks trivial in math land, but if you only have to write 5 lines then you feel a lot better about it

[Patrick Massot]

Rémi Bottinelli said:

(I say simpa because simp doesn't seem to work)

That's presumably because simpa tries reflexivity after doing its work. There was a recent conversation about that where Mario, the author of simpa, was very surprised to learn that everybody was abusing this property, hence completely blurring the intended semantics of simpa

[Rémi Bottinelli]

OK, I'll try and attack the third file coarse_antilipschitz.lean with these new tricks. I think you gave me plenty enough to munch on, @Patrick Massot , thanks!

[Patrick Massot]

Note also that you'll quickly learn how to smell proof inefficiency. There were many proofs in you file where I could see without reading anything carefully that they were wasting a lot of lines doing nothing.

[Kevin Buzzard]

Patrick you should mark some of my student projects!

[Kevin Buzzard]

Have have have have have refl

[Rémi Bottinelli]

https://github.com/bottine/mathlib/blob/31bfb8e72f8a1579ff5ea99b755dc5df42960b07/src/topology/metric_space/coarse/coarse_antilipschitz.lean#L335

[Rémi Bottinelli]

I'm having a "technical" problem here: the term dense has type is_coarsely_dense_with_in L (range f) (univ) and I want to return something of type is_coarsely_dense_with L (range f), which by definition is just is_coarsely_dense_with_in L (range f) (univ)`. I would have thought this is a "defeq" and lean would figure this out, but it seems not. What am I doing wrong?

[Yaël Dillies]

I don't see how that's defeq. true → p is not defeq to p. You probably want to write the lemma whatever_in_univ_iff (and the other direction whatever.whatever_in). See docs#monotone_on_univ and docs#monotone.monotone_on.

[Rémi Bottinelli]

mmh, maybe my question was misguided and I wasn't understanding the error… let me see

[Rémi Bottinelli]

yeah, I think the errors comes from somewhere else. Thanks for the pointers though!

[Rémi Bottinelli]

hah, the culprit was A COMMA, I'm ashamed!

[Daniel Roca González]

Classic!

[Rémi Bottinelli]

great day: I managed to use Zorn's lemma successfully!

[Rémi Bottinelli]

it wasn't even that hard

[Rémi Bottinelli]

OK, what would a good unit for a PR be? I'm close to having one notion of quasi-isometry formalised (quasi-isometric embedding with dense range). In my opinion, assuming the code were clean, this would be a good "semi-atomic" PR, since it defines the basic notions on a space plus one "useful" notion: quasi-isometries (along with it being an equivalence relation).

The WIP code is here.

Some questions:

• There are multiple reasonable definitions of a quasi-isometry: should one define them all with descriptive names, and show equivalence? Which one should be the canonical one? For now I have chosen one, and am just planning on having fun with unicode arrows to distinguish them.
  I think that with the tools defined in my code, showing all equivalences will not be much work, but is it worth it?

• I'm unsure about when to define structures vs properties: Should we have predicates saying that this function is a quasi-isometry, or bundle it somewhere? Similarly, iiuc, equivalence relations follow the refl,symm,trans nomenclature, while "arrows" follow something like self,inv,comp, is that a good rule to go by, in that if an arrow can be inverted, but non-canonically, one should not use inv.

• At some point, I need to use that "being close" for maps is a congruence relation when all (or sufficiently many) maps are coarsely Lipschitz. I feel like using simplifications rules properly and tagging the congruence properties of "closeness" would make things easy to write. The problem is that I think I would need to define a type of "lipschitz maps" on which these congruence rules hold, but it seems a bit heavy to define a new class just for this…

[Johan Commelin]

Re "good unit for a PR": what you describe sounds reasonable. And the file you link to is currently 237 lines, which also seems a good size.
I can't really comment on your other questions atm.

[Patrick Massot]

For quasi-isometry, you should choose one definition, and write lemma proving it is equivalent to other definitions when you need it. Compare with docs#continuous and then docs#continuous_iff_continuous_at and docs#continuous_iff_is_closed.

[Patrick Massot]

The question about bundling is more subtle. It depends how you'll want to use them. Do you primarily want to be able to say that some pre-existing function is a quasi-isom or manipulate the set of quasi-isometries? If unsure then you can start unbundled and then later introduce bundled one. In topology (in mathlib) continuous functions are unbundled almost everywhere, but we do have bundled ones when we want to discuss topologies on spaces of continuous functions. @Anne Baanen may have a preprint for you to read.

[Yaël Dillies]

https://arxiv.org/abs/2202.01629

[Patrick Massot]

Thanks Yaël! I didn't know there was a public version

[Yaël Dillies]

Anne thought I might like the gory details :grinning:

[Kevin Buzzard]

@Yaël Dillies you should post a link to the abstract not the pdf -- at least this is what ArXiv tells everyone (I think there's even a Twitter bot now which nags people about this). The pdfs sometimes get tidied up and the links break; they're then regenerated when someone clicks from the abstract page

[Yaël Dillies]

Oh okay!

[Rémi Bottinelli]

Johan Commelin said:

Re "good unit for a PR": what you describe sounds reasonable. And the file you link to is currently 237 lines, which also seems a good size.
I can't really comment on your other questions atm.

Note that this file uses content of each of space.lean (which I guess should be renamed to basics) and coarse_(anti)lipschitz.lean, so that the whole of it is way larger than 237 lines (not deep content, though).

[Rémi Bottinelli]

Patrick Massot said:

The question about bundling is more subtle. It depends how you'll want to use them. Do you primarily want to be able to say that some pre-existing function is a quasi-isom or manipulate the set of quasi-isometries? If unsure then you can start unbundled and then later introduce bundled one. In topology (in mathlib) continuous functions are unbundled almost everywhere, but we do have bundled ones when we want to discuss topologies on spaces of continuous functions. Anne Baanen may have a preprint for you to read.

Noted. Honestly, I don't really have a clear picture on how I plan to use those definitions exactly… I guess it's when you need to actually use them that you know which way is better.

[Rémi Bottinelli]

RE that paper: doesn't lean4 use a different mechanism for dealing with those, which makes /something/ linear time rather than exponential in lean3 ?

[Patrick Massot]

https://arxiv.org/abs/2001.04301

[Kevin Buzzard]

@Rémi Bottinelli the answer is that PRs of 100 lines are the sort of thing which is preferred, so if your code needs big imports but you have things working then you have evidence that your definitions are usable, so start PRing them in 50-150 line chunks and be prepared for reviews of the form "I believe this definition should be changed (and this will break your code)"; hopefully you have enough evidence to rebut them now. Be warned that the PR process is arduous because the maintainers have extremely high and exacting standards about mathlib's code, an approach which makes it harder to get stuff in mathlib but which has served the community extremely well.

[Rémi Bottinelli]

OK, that makes sense, thanks! I'll take some time to let things settle down, clean the code some more, and then have a look at the PR procedure guide.

[Rémi Bottinelli]

Can I already ask for "write access to non-master branches of the mathlib repository" ? my github handle is bottine.

[Patrick Massot]

done

[Rémi Bottinelli]

Thanks :)

[Kevin Buzzard]

Now you have no excuse not to start :-)

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/pull/12010

[Rémi Bottinelli]

here goes: I hope it's all reasonably OK

[Kevin Buzzard]

It's well over 150 lines (three times as long :-( ) so you might have real problems getting anyone to review it. Can't you just PR the first third somehow?

[Rémi Bottinelli]

three times as long is a no-go? I probably can, but then it's very low content-wise. I assume this should be made as an update to this specific PR ?

[Yaël Dillies]

Also, you have many lines over 100 characters. You'll need to wrap them for style.

[Rémi Bottinelli]

Yeah, it's the comments: my reasoning was that since there would anyway be something to change, I might as well cut the comments in the end.

[Yaël Dillies]

It's really not that hard to keep your comments well trimmed if you're on VScode with the 100 characters guide on.

[Yaël Dillies]

You're introducing many new definitions, some of which you're not using at all. I'd suggest concentrating on fewer and developing more API about them.

[Yaël Dillies]

For example, docs#is_antichain is a really simple notion but I still managed to write 100 lines about it.

[Rémi Bottinelli]

But more API means getting past the 150 lines "soft limit" too, no?

[Yaël Dillies]

That's why you should introduce less definitions :wink:

[Yaël Dillies]

No joke, you have 20 new definitions and one new typeclass. A typical PR adds maybe 3 or 4 of them simultaneously at most.

[Rémi Bottinelli]

I'm unsure now: should I retract the PR, or just update it according to the feedback I get? I don't want to push bad stuff and get people sick too fast

[Kevin Buzzard]

People don't review large PRs because they have 15 minutes for reviews in their spare time and think "golly I'm not looking at that one". Definitions are really hard to get right and need expert opinions. A long PR with lots of new definitions is asking for trouble. Everyone puts it off and then it starts rotting.

[Yaël Dillies]

First, remove all definitions for which you proved no lemma. We definitely won't take those.

[Yaël Dillies]

Second, if there are many left, remove some according to your common sense and keep them for a second PR.

[Kevin Buzzard]

Yeah close the PR and make a smaller one with <= 150 lines of non comment code and ideally <= 100. Also take a look at what the linters say -- nobody will review until your file compiles and lints, and 100+ character lines will stop it linting. The PR process is very hard. There are currently over 300 PRs in progress and it's really important to keep things super-easy for the maintainers especially if you're a new contributer whose code will need some attention

[Yaël Dillies]

I'm not sure the PR itself needs closing. Changes can be done in place. You can always move the surplus stuff to another branch.

[Rémi Bottinelli]

Mmh… Well, I closed it just before you replied, so I guess I'll leave it closed now that it's done. In any case I got some very actionable feedback, which is nice :)

[Rémi Bottinelli]

Thanks to the both of you, and back to the drawing board.

[Kevin Buzzard]

Every definition comes with a cost. Every definition wraps up something in extra wrapping and lean has to figure out whether to unwrap the wrapping or not, and this is hard. Every definition makes terms bigger and more complicated, and this is bad. So every definition has to come with an API which tells lean and users how to use the definition. If you can possibly get away without making a definition, don't make it. If you are making a definition then you need to surround it with theorems. Definitions are costly

[Rémi Bottinelli]

Does that mean that whenever you have a definition, say of the form lipschitz_with \eps, and a non-qualified version lipschitz := \exists \eps lipschitz_with \eps, you should stick to one variant if you don't have a good reason to use both?

[Yaël Dillies]

Exactly

[Rémi Bottinelli]

OK, then there is a lot to cut down already!

[Rémi Bottinelli]

OK, I've shortened it to around 150 lines without comments, and a bit more than 200 with comments. I'll let it sit for a while since I may be rushing things.

[Rémi Bottinelli]

Thinking about it all, I have a few more "theoretical" questions, if you people don't mind:

• RE "definition sparsity": I naturally tend to make a lot of definitions, e.g. just as forms of alias, and to be able to name things. For instance, in the old version of the code, I had a def is_max_blah, which I now inlined in the two functions using it. You might argue that if there is only two places where it's used, this is proof that it doesn't need a def, but at the same time I find it makes things less transparent. So, is there a way to use such "thin" definitions? Does this "definition sparsity" rule stem from an engineering rationale (mathlib being so big a project that some hard rules have to be taken in order to keep things manageable ) ?
• Branches: I see that every time I push to my branch on the mathlib repo, things get rebuilt, which might indicate that these branches are not meant for quick and dirty development. Is that the case?

[Patrick Massot]

You can always use local notations as a thin definition.

[Patrick Massot]

About branches, you can use the building power. That's part of the community infrastructure. Specifically the machines are paid by the Hoskinson center. It's a bit silly to push every three lines, but you can use this infrastructure when you modify a file which is low in the hierarchy and triggers a lot of rebuild.

[Rémi Bottinelli]

Noted, thanks!

[Rémi Bottinelli]

@Patrick Massot In your opinion, how should I deal with this definition, for instance?

[Rémi Bottinelli]

I'm using it to have a nice "bundled" object to reason about when using Zorn.

[Yaël Dillies]

I think this definition should be internal to the proof.

[Rémi Bottinelli]

Indeed, it makes things much more transparent, and allows some shortening: https://github.com/leanprover-community/mathlib/blob/quasi_isometry/src/topology/metric_space/coarse/basic.lean .

[Rémi Bottinelli]

In the doc entry for rcases, there is a part about extracting a witness to the equality with some name, but I'm not sure how it works. What syntax should I use?

[Kyle Miller]

That's for the non-interactive rcases tactic. The interactive syntax is over at tactic#rcases, see the second-to-last paragraph (rcases h : e with PAT)

[Rémi Bottinelli]

Oh, ups, thanks for clearing that up!

[Rémi Bottinelli]

I reopened the PR: hope it's more appropriate now :)