isUnit_of_forall_le_norm_inner_map

English

If f satisfies the bound ∥x∥^2 c ≤ ∥⟪f x, x⟫∥ for some c>0, then f is a unit.

Русский

Если существует c>0 такое, что ∥x∥^2 c ≤ ∥⟪f x, x⟫∥ для всех x, то f является единицей.

LaTeX

$$$\forall x, \|x\|^2 c \le \|⟪f x, x⟫\| \Rightarrow \text{IsUnit}(f)$$$

Lean4

theorem isUnit_of_forall_le_norm_inner_map (f : E →L[𝕜] E) {c : ℝ≥0} (hc : 0 < c)
    (h : ∀ x, ‖x‖ ^ 2 * c ≤ ‖⟪f x, x⟫_𝕜‖) : IsUnit f :=
  by
  rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]
  have h_anti : AntilipschitzWith c⁻¹ f := antilipschitz_of_forall_le_inner_map f hc h
  refine ⟨?_, ⟨_, h_anti⟩⟩
  rw [Submodule.topologicalClosure_eq_top_iff, Submodule.eq_bot_iff]
  intro x hx
  have : ‖x‖ ^ 2 * c = 0 := le_antisymm (by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x) (by positivity)
  aesop

Похожие утверждения