English
If a continuous linear map f satisfies a lower bound relating ∥x∥^2 to ∥⟪f x, x⟫∥ for all x, then f is a unit (bijective with closed range).
Русский
Если для всех x отображение f удовлетворяет неравенству, связывающему ∥x∥^2 с ∥⟪f x, x⟫∥, то f является единицей (биотомно взаимно однозначно отображает пространство).
LaTeX
$$$\text{IsUnit}(f)$ if $\forall x, c\|x\|^2 \le \|⟪f x, x⟫\|$ for some $c>0$; and $f$ has dense range and isantilipschitz.$$
Lean4
theorem antilipschitz_of_forall_le_inner_map {H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : H →L[𝕜] H)
{c : ℝ≥0} (hc : 0 < c) (h : ∀ x, ‖x‖ ^ 2 * c ≤ ‖⟪f x, x⟫_𝕜‖) : AntilipschitzWith c⁻¹ f :=
by
refine f.antilipschitz_of_bound (K := c⁻¹) fun x ↦ ?_
rw [NNReal.coe_inv, inv_mul_eq_div, le_div_iff₀ (by exact_mod_cast hc)]
simp_rw [sq, mul_assoc] at h
by_cases hx0 : x = 0
· simp [hx0]
· apply (map_le_map_iff <| OrderIso.mulLeft₀ ‖x‖ (norm_pos_iff.mpr hx0)).mp
exact (h x).trans <| (norm_inner_le_norm _ _).trans <| (mul_comm _ _).le
