Hofer's lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This is an elementary lemma about complete metric spaces. It is motivated by an application to the bubbling-off analysis for holomorphic curves in symplectic topology. We are very far away from having these applications, but the proof here is a nice example of a proof needing to construct a sequence by induction in the middle of the proof.

References: #

H. Hofer and C. Viterbo, The Weinstein conjecture in the presence of holomorphic spheres

source

@[simp]

theorem pos_div_pow_pos {α : Type u_1} [linear_ordered_semifield α] {a b : α} (ha : 0 < a) (hb : 0 < b) (k : ℕ) :

0 < a / b ^ k

source

theorem hofer {X : Type u_1} [metric_space X] [complete_space X] (x : X) (ε : ℝ) (ε_pos : 0 < ε) {ϕ : X → ℝ} (cont : continuous ϕ) (nonneg : ∀ (y : X), 0 ≤ ϕ y) :

∃ (ε' : ℝ) (H : ε' > 0) (x' : X), ε' ≤ ε ∧ has_dist.dist x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), has_dist.dist x' y ≤ ε' → ϕ y ≤ 2 * ϕ x'