English
A coercive bounded bilinear operator B induces an antilipschitz bound on its associated bilinear form, i.e., there exists C > 0 such that C‖v‖ ≤ ‖B♯v‖ for all v.
Русский
Сила сжатия коэрцитивного ограниченного билинейного отображения B задаёт антиплипшицкое неравенство: найдётся C > 0 such that C‖v‖ ≤ ‖B♯v‖ для всех v.
LaTeX
$$$ ∃ C \in ℝ_{≥0}, 0 < C ∧ ∀ v, C \|v\| ≤ \|B♯ v\|. $$$
Lean4
theorem antilipschitz (coercive : IsCoercive B) : ∃ C : ℝ≥0, 0 < C ∧ AntilipschitzWith C B♯ :=
by
rcases coercive.bounded_below with ⟨C, C_pos, below_bound⟩
refine ⟨C⁻¹.toNNReal, Real.toNNReal_pos.mpr (inv_pos.mpr C_pos), ?_⟩
refine ContinuousLinearMap.antilipschitz_of_bound B♯ ?_
simp_rw [Real.coe_toNNReal', max_eq_left_of_lt (inv_pos.mpr C_pos), ← inv_mul_le_iff₀ (inv_pos.mpr C_pos)]
simpa using below_bound
