Isometric image of finite metric ball

Stream: new members

[Rémi Bottinelli]

Hey! I'm trying to prove that in a transitive metric space, balls have the same cardinality (assuming finite, in my case).
I reckon there should be a very quick way to do this: an isometry restricts to a bijection on balls, which implies equal cardinalities, but I'm not sure how to use what: fintype,finset,injective, maps_to, etc.
How should I proceed here ? And also, is fintype better suited than finset here?

import topology.metric_space.basic
import topology.metric_space.isometry

universe u

open function set fintype function
open_locale nnreal ennreal

variables {α : Type u} [pseudo_metric_space α]

@[class] structure finite_balls :=
(fintype_ball : ∀ x : α, ∀ r : ℝ, fintype (metric.ball x r))

attribute [instance] finite_balls.fintype_ball

def uniformly_finite_balls_with [@finite_balls α _] (k : ℝ → ℕ) :=
∀ x : α, ∀ r : ℝ,  card (metric.ball x r) ≤ k r

namespace uniformly_finite_balls_with

lemma of_transitive
  [inhabited α]
  [@finite_balls α _]
  (tr : ∀ x y : α, ∃ f : α ≃ᵢ α, (f x = y)) :
  ∃ k : ℝ → ℕ, @uniformly_finite_balls_with α _ _ k :=
begin
  let x := arbitrary α,
  let k := λ r, card $ metric.ball x r,
  use k,
  intros y r,
  rcases tr x y with ⟨fᵢ,fxy⟩,
  rw ←fxy,
  rw ← isometric.image_ball fᵢ x r, -- doesn't work
end

end uniformly_finite_balls_with

[Vincent Beffara]

finset.card_image_of_injective ?

[Rémi Bottinelli]

Does that mean I should change my defs to use finset, or is it fine as it is?

[Rémi Bottinelli]

lemma of_transitive
  [inhabited α]
  (fb : @finite_balls α _)
  (tr : ∀ x y : α, ∃ f : α ≃ᵢ α, (f x = y)) :
  ∃ k : ℕ → ℕ, @uniformly_finite_balls_with α _ _ k :=
begin
  let x := arbitrary α,
  let k := λ (r : ℕ), card (metric.ball x r),
  use k,
  intros y r,
  rcases tr x y with ⟨fᵢ,fxy⟩,
  rw ←fxy,
  have Bxrfintype : fintype (metric.ball x r), by {sorry},
  have Byrfintype : fintype (metric.ball y r), by {sorry},
  have lol1 := isometric.image_ball fᵢ x r, -
  have imgffintype : fintype ↥(⇑fᵢ '' metric.ball x ↑r), by {sorry},
  have lol3 : card (metric.ball x r) ≤ k r, by {simp},
  have lol4 := @card_image_of_injective α α (metric.ball x r) Bxrfintype fᵢ imgffintype (isometric.injective fᵢ),
  simp_rw lol1 at lol4,
  rw lol4,
  exact lol3,
end

I think that's a contender for ugliest non-working code. After some search on zulip, it seems part of the problem is that the elaborator doesn't handle the fintype instances in the way I'd like it to.

[Yaël Dillies]

Those have should be haveI

[Rémi Bottinelli]

lemma of_transitive
  [inhabited α]
  [fb : @finite_balls α _]
  (tr : ∀ x y : α, ∃ f : α ≃ᵢ α, (f x = y)) :
  ∃ k : ℕ → ℕ, @uniformly_finite_balls_with α _ _ k :=
begin
  let x := arbitrary α,
  let k := λ (r : ℕ), card (metric.ball x r),
  use k,
  intros y r,
  rcases tr x y with ⟨fᵢ,fxy⟩,
  rw ←fxy,
  have Bxrfintype : fintype (metric.ball x r), by {sorry},
  have Byrfintype : fintype (metric.ball y r), by {sorry},
  have imgisball:= isometric.image_ball fᵢ x r,
  have imgffintype : fintype ↥(⇑fᵢ '' metric.ball x ↑r), from set.fintype_image _ fᵢ,
  have := @card_image_of_injective _ _ (metric.ball x r) _ fᵢ imgffintype (isometric.injective fᵢ),
  simp_rw [imgisball,this] at *,
end

[Rémi Bottinelli]

OK, only two sorries, which I feel should come for free?

[Rémi Bottinelli]

oh, thanks, haveI looks to be part of what I was missing!

[Rémi Bottinelli]

ah, I'm getting there, let me see

[Rémi Bottinelli]

lemma of_transitive
  [inhabited α]
  [fb : @finite_balls α _]
  (tr : ∀ x y : α, ∃ f : α ≃ᵢ α, (f x = y)) :
  ∃ k : ℕ → ℕ, @uniformly_finite_balls_with α _ _ k :=
begin
  let x := arbitrary α,
  let k := λ (r : ℕ), card (metric.ball x r),
  use k,
  intros y r,
  rcases tr x y with ⟨fᵢ,fxy⟩,
  rw ←fxy,
  have imgisball := isometric.image_ball fᵢ x r,
  have imgcard   := card_image_of_injective (metric.ball x r) (isometric.injective fᵢ),
  simp_rw [imgisball,imgcard] at *,
end

I believe that's close enough! Thanks for the help!

[Rémi Bottinelli]

And by the way, it seems that lean doesn't accept unfolding definitions when they are not made properly as a def.
Say in the code above, I can't unfold k. What's the reason for this?

[Sebastien Gouezel]

The mathlib way would probably be to split this into several lemmas:

• if there is an isometric equivalence between two spaces, mapping x to y, then the cardinality (in the sense of cardinal numbers) of ball x r and ball y r are the same.
• If additionally ball x r is finite, then ball y r is also finite
• and their cardinalities as finite sets are the same