Hofer's lemma #
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
@[simp]
theorem
pos_div_pow_pos
{α : Type u_1}
[LinearOrderedSemifield α]
{a : α}
{b : α}
(ha : 0 < a)
(hb : 0 < b)
(k : ℕ)
: