Small enough balls

Stream: Is there code for X?

[Vincent Beffara]

Do we have this somewhere in a metric_space?

lemma eventually_iff_eventually_norm' :
  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ ball z₀ r, P z) := sorry

I have an ugly epsilon-delta proof but I'm guessing that it is a one-line proof using the filter API properly...

[Junyan Xu]

should be easy from docs#metric.eventually_nhds_iff_ball

[Vincent Beffara]

Aka docs#metric.mem_nhds_iff yes sure, this is what I am doing now:

lemma eventually_iff_eventually_norm :
  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝 0, ∀ z ∈ ball z₀ r, P z) :=
begin
  refine metric.mem_nhds_iff.trans (iff.trans _ metric.mem_nhds_iff.symm),
  split,
  { rintro ⟨ε, hε, h⟩,
    refine ⟨ε, hε, λ r hr z hz, _⟩,
    simp only [mem_ball_zero_iff, real.norm_eq_abs] at hr,
    exact h (ball_subset_ball ((le_abs_self r).trans hr.le) hz) },
  { rintro ⟨ε, hε, h⟩,
    refine ⟨ε, hε, λ z hz, _⟩,
    obtain ⟨ρ, hρ⟩ := nonempty_Ioo.mpr (mem_ball.mp hz),
    have : ρ ∈ ball (0 : ℝ) ε,
    by simp only [_root_.abs_of_nonneg (dist_nonneg.trans hρ.1.le), hρ.2, mem_ball_zero_iff,
      real.norm_eq_abs],
    exact h this z hρ.1 }
end

but it feels overly complicated. (Well this is for the version without the [>] but that should be similar.)

[Jireh Loreaux]

the other trick will be to use a filter basis for 𝓝[>] 0 I think, along with docs#filter.has_basis.eventually.

[Vincent Beffara]

I end up doing archimedean stuff like this:

lemma toto : (∀ y, |y| < ε → 0 < y → ∀ z, dist z z₀ < y → P z) ↔
  (∀ z, dist z z₀ < ε → P z) :=
begin
  split,
  { rintro h z hz,
    obtain ⟨ρ, hρ⟩ := nonempty_Ioo.mpr hz,
    have h1 : 0 < ρ := dist_nonneg.trans_lt hρ.1,
    have h2 : |ρ| = ρ := abs_eq_self.mpr h1.le,
    exact h ρ (h2.symm ▸ hρ.2) h1 z hρ.1 },
  { rintro h y h1 h2 z hz,
    exact h z (hz.trans (lt_of_abs_lt h1)) }
end

lemma eventually_iff_eventually_norm' :
  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ ball z₀ r, P z) :=
begin
  simp [eventually_nhds_within_iff, eventually_nhds_iff_ball, toto],
end

[Jireh Loreaux]

Here it is with the approach I suggested. There's still a bit of fussing you have to do after the rewrites, but it's pretty minimal.

open_locale filter topological_space
open metric filter

variables {X : Type*} [metric_space X] (z₀ : X) (P : X → Prop)

lemma eventually_iff_eventually_norm' :
  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ ball z₀ r, P z) :=
begin
  rw [(nhds_within_has_basis nhds_basis_closed_ball (set.Ioi (0 : ℝ))).eventually_iff,
    eventually_nhds_iff_ball],
  simp only [real.closed_ball_eq_Icc, gt_iff_lt, exists_prop, zero_sub, zero_add,
    set.mem_inter_iff, set.mem_Icc, set.mem_Ioi, and_imp],
  congrm ∃ ε : ℝ, _,
  exact ⟨λ h, ⟨h.1, λ x _ hxε _ z hz, h.2 z (ball_subset_ball hxε hz)⟩,
    λ h, ⟨h.1, h.2 (neg_lt_self h.1).le le_rfl h.1⟩⟩,
end

[Anatole Dedecker]

I don't have time to give a solution right now, but let me just say that what we are really proving is (𝓝 z₀).small_sets = (𝓝[>] 0 : filter ℝ).map (ball z₀) (see docs#filter.eventually_small_sets_forall), but I'm not sure how to make this easy yet

[Junyan Xu]

Here's my proof:

import topology.metric_space.basic
open_locale topological_space
open metric

lemma eventually_iff_eventually_norm {α} [pseudo_metric_space α] {z₀ : α} {P : α → Prop} :
  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝 0, ∀ z ∈ ball z₀ r, P z) :=
begin
  simp_rw eventually_nhds_iff_ball,
  refine exists₂_congr (λ r hr, ⟨λ h y hy z hz, _, λ h y hy, _⟩),
  { rw [real.ball_eq_Ioo, zero_add] at hy,
    exact h z (ball_subset_ball hy.2.le hz) },
  { obtain ⟨r', hr', hr⟩ := exists_between hy, -- exists_lt_mem_ball_of_mem_ball is defeq
    refine h r' _ y hr',
    rw [ball, set.mem_set_of, real.dist_0_eq_abs, abs_eq_self.2],
    exacts [hr, dist_nonneg.trans hr'.le] },
end

[Junyan Xu]

Maybe you can golf it further using ideas in other approaches.

[Vincent Beffara]

variables {α β : Type*} [metric_space α] {z₀ : α} {P : α → Prop} {ε : ℝ} {s : set α}

lemma tititi : s ∈ 𝓝 z₀ ↔ ∀ᶠ r in 𝓝[>] 0, ball z₀ r ⊆ s :=
begin
  rw [(nhds_within_has_basis nhds_basis_closed_ball (Ioi (0 : ℝ))).eventually_iff],
  simp_rw [metric.mem_nhds_iff, mem_inter_iff, mem_closed_ball_zero_iff, ← exists_prop],
  exact exists₂_congr (λ ε hε, ⟨λ h r ⟨hr, hh⟩, (ball_subset_ball (le_of_abs_le hr)).trans h,
    λ h, h ⟨(abs_eq_self.mpr hε.lt.le).le, hε⟩⟩)
end

lemma eventually_iff_eventually_norm' :
  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ ball z₀ r, P z) :=
tititi

[Vincent Beffara]

Actually, this might look a bit better:

variables {α : Type*} {z₀ : α} {P : α → Prop} {s : set α} {p : filter α} {φ : ℝ → set α}

lemma mem_iff_eventually_subset (hp : p.has_basis (λ t:ℝ, 0 < t) φ) (hφ : monotone φ) :
  s ∈ p ↔ ∀ᶠ t in 𝓝[>] 0, φ t ⊆ s :=
begin
  rw [(nhds_within_has_basis nhds_basis_closed_ball (Ioi (0 : ℝ))).eventually_iff],
  simp_rw [hp.mem_iff, ← exists_prop, mem_inter_iff, mem_closed_ball_zero_iff],
  refine exists₂_congr (λ ε hε, ⟨λ h r h', (hφ (le_of_abs_le h'.1)).trans h,
    λ h, h ⟨eq.le (abs_eq_self.mpr hε.le), hε⟩⟩)
end

lemma eventually_nhds_iff_eventually_ball [metric_space α] :
  (∀ᶠ z in 𝓝 z₀, P z) ↔ (∀ᶠ r in 𝓝[>] 0, ∀ z ∈ ball z₀ r, P z) :=
mem_iff_eventually_subset nhds_basis_ball (λ _ _, ball_subset_ball)