Hofer's lemma

Stream: general

[Kevin Buzzard]

Wow so what's the de Bruijn factor here?

[Johan Commelin]

~ 70/7 = 10 ??

[Bryan Gin-ge Chen]

The gzipped size of Mario's proof is 1764 bytes and the gzipped size of the corresponding LaTeX source is 606 bytes. Based on that the de Bruijn factor is 2.91.

(Here's the bit of the LaTeX I used):

\begin{lemma}[Hofer]
\label{lemma:Hofer}
Suppose $(X,d)$ is a complete metric space, $g : X \to [0,\infty)$ is
continuous, $x_0 \in X$ and $\epsilon_0 > 0$.  Then there exist
$x \in X$ and $\epsilon > 0$ such that,
\begin{enumerate}
\renewcommand{\labelenumi}{(\alph{enumi})}
\item $\epsilon \le \epsilon_0$,
\item $g(x) \epsilon \ge g(x_0) \epsilon_0$,
\item $d(x,x_0) \le 2\epsilon_0$, and
\item $g(y) \le 2 g(x)$ for all $y \in \overline{B_\epsilon(x)}$.
\end{enumerate}
\end{lemma}
\begin{proof}
If there is no $x_1 \in \overline{B_{\epsilon_0}(x_0)}$ such that
$g(x_1) > 2 g(x_0)$, then we can set $x = x_0$ and $\epsilon = \epsilon_0$
and are done.  If such a point~$x_1$ does exist, then we
set $\epsilon_1 := \epsilon_0 / 2$ and repeat the above process for the
pair $(x_1,\epsilon_1)$: that is, if there is no $x_2 \in
\overline{B_{\epsilon_1}(x_1)}$ with $g(x_2) > 2 g(x_1)$, we set
$(x,\epsilon) = (x_1,\epsilon_1)$ and are finished, and
otherwise define $\epsilon_2 = \epsilon_1 / 2$ and repeat for
$(x_2,\epsilon_2)$.  This process must eventually terminate, as otherwise
we obtain a Cauchy sequence $x_n$ with $g(x_n) \to \infty$, which is
impossible if~$X$ is complete.
\end{proof}

[Bryan Gin-ge Chen]

This follows (my interpretation of) the rules on Freek Wiedijk's page.

[Kevin Buzzard]

Oh so it is better than I (and Johan) thought!

[Johan Commelin]

I just counted lines... roughly

[Kevin Buzzard]

Right, so did i

[Patrick Massot]

I'm still working on getting a nicer proof. But each time I think I'm almost done, there is something very slightly off.

[David Wärn]

For what it's worth, here is an approach that avoids classical.epsilon by using a predicate on X x R which guarantees that we can safely move to the next step.

import topology.metric_space.basic
open_locale classical topological_space

lemma hofer {X : Type} [metric_space X] [complete_space X]
  (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ} (cont : continuous φ) (nonneg : ∀ x, 0 ≤ φ x) :
∃ (ε' > 0) (x' : X), ε' ≤ ε ∧
                   dist x' x ≤ 2*ε ∧
                   ε * φ x ≤ ε' * φ x' ∧
                   ∀ y, dist x' y ≤ ε' → φ y ≤ 2*φ x' :=
begin
  by_contra H,
  set Y : set (X × ℝ) :=
    { p : X × ℝ | 0 < p.2 ∧ p.2 ≤ ε
                ∧ dist p.1 x ≤ 2 * ε - 2 * p.2
                ∧ ε * φ x ≤ p.2 * φ p.1 },
  have xε_mem_Y : (x, ε) ∈ Y := ⟨ε_pos, le_refl _, by simp, le_refl _⟩,
  have dist_le_2ε : ∀ (p ∈ Y), dist (p.1 : X) x ≤ 2 * ε,
  { rintros ⟨y, r⟩ ⟨r_pos, _, hd, _⟩,
    calc dist y x ≤ 2 * ε - 2 * r : hd
              ... ≤ 2 * ε         : by linarith },
  have key : ∀ (p : Y), ∃ (q : Y), dist (p.val.1 : X) q.val.1 ≤ p.val.2
                              ∧ 2 * φ p.val.1 < φ q.val.1,
  { rintros ⟨⟨y, r⟩, r_pos, r_le, hd, hp⟩,
    have hyr : (y, r) ∈ Y := ⟨r_pos, r_le, hd, hp⟩,
    by_contra N,
    apply H,
    refine ⟨r, r_pos, y, r_le, dist_le_2ε _ hyr, hp, _⟩,
    intros z hz,
    push_neg at N,
    by_contra b,
    push_neg at b,
    have : (z, r / 2) ∈ Y,
    { refine ⟨half_pos r_pos, _, _, _⟩,
      calc r / 2 ≤ r : by linarith
             ... ≤ ε : r_le,
      calc dist z x ≤ dist y z + dist y x : dist_triangle_left _ _ _
                ... ≤ r + (2 * ε - 2 * r) : add_le_add hz hd
                ... = 2 * ε - 2 * (r / 2) : by ring,
      apply le_of_lt,
      calc ε * φ x ≤ r * φ y             : hp
               ... = (r / 2) * (2 * φ y) : by ring
               ... < (r / 2) * φ z       : mul_lt_mul_of_pos_left b (half_pos r_pos), },
    cases N ⟨_, this⟩,
    { refine lt_irrefl r _,
      calc r < dist y z : h
         ... ≤ r        : hz },
    { refine lt_irrefl (φ z) _,
      calc φ z ≤ 2 * φ y : h
           ... < φ z     : b }, },
  set f : Y → Y := λ p, classical.some (key p),
  set xi : ℕ → Y := λ n, f^[n] ⟨_, xε_mem_Y⟩,
  sorry, /- TODO: show that `φ (xi n).val.1` grows exponentially, deduce that
              `(xi n).val.2` decays exponentially, and hence that
              `dist (xi n).val.1 (xi (n+1)).val.1` decays exponentially, contradiction -/
end

[David Wärn]

Having thought about this a bit, I don't think this is a case for Baire, nor for #2850.

[Patrick Massot]

I have a version that I find not too bad. It uncovered a lot of small lemmas that are either holes in mathlib or proving I don't know how to search mathlib. I'd be interested to know what's already hidden somewhere.

import analysis.specific_limits
import tactic.ring_exp

open_locale classical topological_space big_operators
open filter set classical finset

local notation `d` := dist

@[simp]
lemma pos_of_div_pow_two {ε : ℝ} (hε : 0 < ε) (k : ℕ) : 0 < ε/2^k :=
begin
  apply div_pos hε,
  exact_mod_cast nat.pow_pos (by norm_num : 0 < 2) k,
end

@[simp]
lemma nonneg_of_div_pow_two {ε : ℝ} (hε : 0 < ε) (k : ℕ) : 0 ≤ ε/2^k :=
begin
  have := pos_of_div_pow_two hε k,
  linarith,
end

@[simp]
lemma help {ε : ℝ} (hε : 0 < ε) (k : ℕ) : ε/2^k ≤ ε :=
begin
  have : (0 : ℝ) < 2^k,
  { apply pow_pos,
    norm_num },
  rw div_le_iff this,
  calc ε = ε *1 : by simp
      ...  ≤ ε*2^k : by {rw mul_le_mul_left _, apply one_le_pow_of_one_le, norm_num, assumption},
end
open set

lemma inf_eq_bot_iff {α : Type*} {f g : filter α} :
  f ⊓ g = ⊥ ↔ ∃ U V, (U ∈ f) ∧ (V ∈ g) ∧ U ∩ V = ∅ :=
begin
  rw ← not_iff_not,
  simp only [not_exists],
  convert inf_ne_bot_iff,
  rw forall_congr,
  intro U,
  rw forall_congr,
  intro V,
  rw ← ne_empty_iff_nonempty ,
  tauto,
end

lemma Ioo_mem_nhds {r : ℝ} (x : ℝ) (h : 0 < r) : Ioo (x - r) (x + r) ∈ 𝓝 x :=
begin
  simp_rw [mem_nhds_iff_exists_Ioo_subset, mem_Ioo],
  refine ⟨x-r, x+r, _, subset.refl _⟩,
  split ; linarith,
end

lemma Ioi_mem_at_top (x : ℝ) : Ioi x ∈ (at_top : filter ℝ) :=
begin
  apply mem_sets_of_superset (mem_at_top (x+1)),
  intros y h,
  change x+1 ≤ y at h,
  rw mem_Ioi,
  linarith,
end

lemma inf_nhds_at_top  (x : ℝ) : 𝓝 x ⊓ at_top = ⊥ :=
begin
  rw inf_eq_bot_iff,
  use [Ioo (x-1) (x+1), Ioi (x+2), Ioo_mem_nhds x (by norm_num), Ioi_mem_at_top _],
  ext y,
  simp,
  intros,
  linarith
end

lemma not_tendsto_nhds_of_tendsto_at_top {α : Type*} {F : filter α} (hF : F ≠ ⊥) {f : α → ℝ} (hf : tendsto f F at_top) (x : ℝ) :
¬ tendsto f F (𝓝 x) :=
begin
  intros h,
  rw tendsto at *,
  have : map f F ≤ 𝓝 x ⊓ at_top,
    from le_inf h hf,
  exact ne_bot_of_le_ne_bot (map_ne_bot hF) this (inf_nhds_at_top _),
end

lemma not_tendsto_at_top_of_tendsto_nhds {α : Type*} {F : filter α} (hF : F ≠ ⊥) {f : α → ℝ}  {x : ℝ} (hf : tendsto f F (𝓝 x)) :
¬ tendsto f F at_top :=
λ h', not_tendsto_nhds_of_tendsto_at_top hF h' x hf

-- This is a variation on `nat.case_strong_induction_on` that doesn't pollute the goal with n.succ
protected lemma nat.case_strong_induction_on' {p : nat → Prop} (a : nat)
  (hz : p 0)
  (hi : ∀ n, (∀ m, m ≤ n → p m) → p (n + 1)) : p a :=
nat.case_strong_induction_on _ hz hi

lemma geom_lt {u : ℕ → ℝ} {k : ℝ} (hk : 0 < k) {n : ℕ} (h : ∀ m ≤ n, k*u m < u (m + 1)) :
k^(n + 1) *u 0 < u (n + 1) :=
begin

 induction n with n ih,
 simp,
 exact h 0 (le_refl _),
 have : (∀ (m : ℕ), m ≤ n → k * u m < u (m + 1)),
   intros m hm, apply h, exact nat.le_succ_of_le hm,
 specialize ih this,
 change k ^ (n + 2) * u 0 < u (n + 2),
 replace h : k * u (n + 1) < u (n + 2) := h (n+1) (le_refl _),
 calc k ^ (n + 2) * u 0 = k*(k ^ (n + 1) * u 0) : by ring_exp
  ... < k*(u (n + 1)) : mul_lt_mul_of_pos_left ih hk
  ... < u (n + 2) : h,
end

lemma finset.sum_map_mul_right {α : Type*} {β : Type*} [semiring β] {b : β} {s : finset α} {f : α → β} :
  ∑ a in s, f a * b = (∑ a in s, f a) * b :=
multiset.sum_map_mul_right

lemma sum_geometric_two_le (n : ℕ) : ∑ (i : ℕ) in range n, (1 / (2 : ℝ)) ^ i ≤ 2 :=
begin
  have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i,
  { intro i, apply pow_nonneg, norm_num },
  convert sum_le_tsum (range $ n) (λ i _, this i) summable_geometric_two,
  exact tsum_geometric_two.symm
end

lemma dist_le_of_geometric_aux {X : Type} [metric_space X] {u : ℕ → X} {n : ℕ} {ε : ℝ}
  (h : ∀ m ≤ n, d (u m) (u (m+1)) ≤ ε/2^m) : d (u 0) (u (n + 1)) ≤ 2 * ε :=
have hε : 0 ≤ ε,
  from calc 0 ≤ d (u 0) (u (0 + 1)) : dist_nonneg
          ... ≤ _ : by simpa using h 0 (zero_le _),
let r := range (n+1) in
calc
d (u 0) (u (n + 1))
    ≤ ∑ i in r, d (u i) (u $ i+1) : dist_le_range_sum_dist u (n + 1)
... ≤ ∑ i in r, ε/2^i             : sum_le_sum (λ i i_in, h i $
                                                nat.lt_succ_iff.mp $ finset.mem_range.mp i_in)
... = ∑ i in r, (1/2)^i*ε         : by {congr, ext i, field_simp }
... = (∑ i in r, (1/2)^i)*ε       : finset.sum_map_mul_right
... ≤ 2*ε                         : mul_le_mul_of_nonneg_right (sum_geometric_two_le _) hε

lemma tendsto_at_top_of_geom_lt {v : ℕ → ℝ} {k : ℝ} (h₀ : 0 < v 0) (hk : 1 < k)
  (hu : ∀ n, k*v n < v (n + 1)) : tendsto v at_top at_top :=
begin
  apply tendsto_at_top_mono,
  show ∀ n, k^n*v 0 ≤ v n,
  { intro n,
    induction n with n ih,
    simp,
    calc k ^ (n + 1) * v 0 = k*(k^n*v 0) : by ring_exp
    ... ≤ k*v n : mul_le_mul_of_nonneg_left ih (by linarith)
    ... ≤ v (n + 1) : le_of_lt (hu n) },
  apply tendsto_at_top_mul_right h₀,
  exact tendsto_pow_at_top_at_top_of_gt_1 hk,
end

lemma hofer {X: Type} [metric_space X] [complete_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ} (cont : continuous φ) (nonneg : ∀ y, 0 ≤ φ y) :
∃ (ε' > 0) (x' : X), ε' ≤ ε ∧
                   dist x' x ≤ 2*ε ∧
                   ε * φ x ≤ ε' * φ x' ∧
                   ∀ y, dist x' y ≤ ε' → φ y ≤ 2*φ x' :=
begin
  by_contradiction H,
  have reformulation : ∀ x' (k : ℕ), ε * φ x ≤ ε / 2 ^ k * φ x' ↔ 2^k * φ x ≤ φ x',
  { intros x' k,
    rw [div_mul_eq_mul_div, le_div_iff, mul_assoc, mul_le_mul_left ε_pos, mul_comm],
    exact pow_pos (by norm_num) k, },
  replace H : ∀ k : ℕ, ∀ x', ∃ y,
    d x' x ≤ 2 * ε ∧ 2^k * φ x ≤ φ x' → d x' y ≤ ε/2^k ∧ 2 * φ x' < φ y,
  { intros k x',
    by_cases h' : d x' x ≤ 2 * ε ∧ 2^k * φ x ≤ φ x',
    { contrapose H,
      rw not_not,
      use ε/2^k,
      simp [ε_pos],
      use x',
      simpa [h'.left, reformulation,  h'.right, h'] using H },
    { use x } },
  clear reformulation,
  choose F hF using H,
  let u : ℕ → X := λ n, nat.rec_on n x F,
  have hu :
    ∀ n,
      d (u n) x ≤ 2 * ε ∧ 2^n * φ x ≤ φ (u n) →
      d (u n) (u $ n + 1) ≤ ε / 2 ^ n ∧ 2 * φ (u n) < φ (u $ n + 1),
  { intro n,
    exact hF n (u n) },
  clear hF,
  have key : ∀ n, d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * φ (u n) < φ (u (n + 1)),
  { intro n,
    induction n using nat.case_strong_induction_on' with n IH,
    { specialize hu 0,
      simp [show u 0 = x, from rfl, le_refl] at *,
      exact hu (by linarith) },
    have A : d (u (n+1)) x ≤ 2 * ε,
    { rw [dist_comm],
      exact dist_le_of_geometric_aux (λ k hk, (IH k hk).1), },
    have B : 2^(n+1) * φ x ≤ φ (u (n + 1)),
    { apply le_of_lt,
      exact geom_lt (by norm_num) (λ  m hm, (IH _ hm).2), },
    exact hu (n+1) ⟨A, B⟩, },
  cases forall_and_distrib.mp key with key₁ key₂,
  have cauchy_u : cauchy_seq u,
  { apply cauchy_seq_of_le_geometric _ ε (by norm_num : 1/(2:ℝ) < 1),
    intro n,
    convert key₁ n,
    simp },
  obtain ⟨y, limy⟩ : ∃ y, tendsto u at_top (𝓝 y),
    from complete_space.complete cauchy_u,
  have lim_top : tendsto (φ ∘ u) at_top at_top,
  { let v := λ n, (φ ∘ u) (n+1),
    suffices : tendsto v at_top at_top,
      by rwa tendsto_add_at_top_iff_nat at this,
    have hv₀ : 0 < v 0,
    { have : 0 ≤ φ (u 0) := nonneg x,
      calc 0 ≤ 2 * φ (u 0) : by linarith
      ... < φ (u (0 + 1)) : key₂ 0 },
    apply tendsto_at_top_of_geom_lt hv₀ (by norm_num : (1 : ℝ) < 2),
    exact λ n, key₂ (n+1) },
  have lim : tendsto (φ ∘ u) at_top (𝓝 (φ y)),
    from tendsto.comp cont.continuous_at limy,
  exact not_tendsto_at_top_of_tendsto_nhds at_top_ne_bot lim lim_top,
end

[Patrick Massot]

Now I'll look at David's version.

[Patrick Massot]

It's an interesting version, especially since it can be shortened by using linarith in three places. But the coercions to sort, .val and .1 are really not pretty. I'd be curious to see what it becomes if you stop pretending in the beginning that you won't use ε/2^k. And of course I'd be also interested to see whether this setup allows to go nicely through the end of the proof.

[Patrick Massot]

I started to try to "fix" this version, but it turns out I'm essentially only rewriting it into my version...

[Mario Carneiro]

I think I had the same problem in my proof. I started out with a sequence similar to the paper proof, but you need to know that the epsilon sequence is ε/2^k or something almost as strong in order to prove that the sequence converges to zero

[Mario Carneiro]

I also haven't really used much of the library around limits and metric spaces so the proof was very low level

[Reid Barton]

Here is a crec version, borrowing some parts of Patrick's proof:

import topology.metric_space.basic
import analysis.specific_limits
import tactic.ring_exp
import .crec

open filter
open_locale classical topological_space

lemma tendsto_at_top_of_geom_lt {v : ℕ → ℝ} {k : ℝ} (h₀ : 0 < v 0) (hk : 1 < k)
  (hu : ∀ n, k*v n < v (n + 1)) : tendsto v at_top at_top :=
sorry -- from Patrick's proof

lemma not_tendsto_at_top_of_tendsto_nhds {α : Type*} {F : filter α} (hF : F ≠ ⊥) {f : α → ℝ}  {x : ℝ} (hf : tendsto f F (𝓝 x)) :
¬ tendsto f F at_top :=
sorry -- from Patrick's proof

lemma div_le_self {α β : ℝ} (hα : α ≥ 0) (hβ : β > 0) : α / β ≤ α := sorry

inductive is_succ : ℕ → ℕ → Prop
| mk (n) : is_succ n (n+1)

lemma wf_is_succ : well_founded is_succ := sorry

lemma hofer {X: Type} [metric_space X] [complete_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε)
  {φ : X → ℝ} (cont : continuous φ) (nonneg : ∀ x, 0 ≤ φ x) :
∃ (ε' > 0) (x' : X)
  (h : ε' ≤ ε ∧
       dist x' x ≤ 2*ε ∧
       ε * φ x ≤ ε' * φ x'),
  ∀ y, dist x' y ≤ ε' → φ y ≤ 2*φ x' :=
begin
  by_contradiction H,
  simp only [not_exists, not_forall] at H,
  -- conditions imposed at the nth step
  let C : Π (n : ℕ), Type :=
    λ n, {x' : X // dist x' x ≤ 2 * (1 - 1 / 2^n) * ε ∧ 2^n * φ x ≤ φ x'},
  -- conditions imposed on consecutive steps
  let q : Π (n₁ n₂ : ℕ) (h : is_succ n₁ n₂) (x₁ : C n₁) (x₂ : C n₂), Prop :=
    λ n₁ n₂ h x₁ x₂, dist x₁.val x₂.val ≤ ε / 2^n₁ ∧ 2 * φ x₁ < φ x₂,
  -- construct a sequence satisfying all the conditions
  let f : Π (n : ℕ), C n,
  { refine crec wf_is_succ q _,
    intros n IH,
    cases n with n,
    { refine ⟨⟨x, _, _⟩, _⟩,
      { simp },
      { simp },
      rintros _ ⟨⟩ },
    { let x' := (IH.val n (is_succ.mk n)).val,
      obtain ⟨hx'₁, hx'₂⟩ := (IH.val n (is_succ.mk n)).property,
      have := H (ε / 2^n) (div_pos ε_pos (pow_pos two_pos _)) x'
        ⟨div_le_self (le_of_lt ε_pos) (pow_pos two_pos _), _, _⟩,
      choose y hy₁ hy₂ using this,
      refine ⟨⟨y, _, _⟩, _⟩,
      { have : dist y x ≤ dist x' y + dist x' x := dist_triangle_left _ _ _,
        have : ε / 2^n + 2 * (1 - 1 / 2^n) * ε = 2 * (1 - 1 / 2^n.succ) * ε,
        { change n.succ with n+1, ring_exp, field_simp, ring },
        linarith },
        { rw [pow_succ, mul_assoc], linarith },
      { rintros _ ⟨⟩,
        refine ⟨hy₁, lt_of_not_ge hy₂⟩ },
      { refine le_trans hx'₁ _,
        rw [mul_le_mul_right ε_pos, mul_le_iff_le_one_right two_pos],
        apply le_of_lt,
        apply sub_lt_self,
        exact (div_pos zero_lt_one (pow_pos two_pos _)) },
      { calc
          ε * φ x = ε / 2 ^ n * (2 ^ n * φ x) : by { field_simp, ring }
              ... ≤ ε / 2 ^ n * φ _ :
            by { rwa mul_le_mul_left (div_pos ε_pos (pow_pos two_pos _)) } } } },
  have hf : Π (n : ℕ), q n (n+1) (is_succ.mk n) (f n) (f (n+1)) :=
    λ n, crec_consistent wf_is_succ q _ n (n+1) (is_succ.mk n),
  let u : ℕ → X := λ n, (f n).1,
  -- rest adapted from Patrick's proof
  have cauchy_u : cauchy_seq u,
  { apply cauchy_seq_of_le_geometric_two (ε * 2),
    intro n,
    convert (hf n).1,
    field_simp },
  obtain ⟨y, limy⟩ : ∃ y, tendsto u at_top (𝓝 y),
    from complete_space.complete cauchy_u,
  have lim_top : tendsto (φ ∘ u) at_top at_top,
  { let v := λ n, (φ ∘ u) (n+1),
    suffices : tendsto v at_top at_top,
      by rwa tendsto_add_at_top_iff_nat at this,
    have hv₀ : 0 < v 0,
    { have : 0 ≤ φ (u 0) := nonneg _,
      calc 0 ≤ 2 * φ (u 0) : by linarith
      ... < φ (u (0 + 1)) : (hf 0).2 },
    apply tendsto_at_top_of_geom_lt hv₀ (by norm_num : (1 : ℝ) < 2),
    exact λ n, (hf (n+1)).2 },
  have lim : tendsto (φ ∘ u) at_top (𝓝 (φ y)),
    from tendsto.comp cont.continuous_at limy,
  exact not_tendsto_at_top_of_tendsto_nhds at_top_ne_bot lim lim_top,
end