English
If a linear map is bounded on a ball of radius r, then there exists a global bound with a constant depending on r that controls ∥f z∥ by ∥z∥.
Русский
Если линейное отображение ограничено на шаре радиуса r, то существует глобальная граница: ∥f z∥ ≤ C ∥z∥ для всех z, где C зависит от r.
LaTeX
$$$\\exists C>0\\ \\forall z:\\, E,\\; \\|f z\\| \\le C \\|z\\|.$$$
Lean4
theorem antilipschitz_of_comap_nhds_le [h : RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) (hf : (𝓝 0).comap f ≤ 𝓝 0) :
∃ K, AntilipschitzWith K f :=
by
rcases ((nhds_basis_ball.comap _).le_basis_iff nhds_basis_ball).1 hf 1 one_pos with ⟨ε, ε0, hε⟩
simp only [Set.subset_def, Set.mem_preimage, mem_ball_zero_iff] at hε
lift ε to ℝ≥0 using ε0.le
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
refine ⟨ε⁻¹ * ‖c‖₊, AddMonoidHomClass.antilipschitz_of_bound f fun x => ?_⟩
by_cases hx : f x = 0
· rw [← hx] at hf
obtain rfl : x = 0 :=
Specializes.eq
(specializes_iff_pure.2 <| ((Filter.tendsto_pure_pure _ _).mono_right (pure_le_nhds _)).le_comap.trans hf)
exact norm_zero.trans_le (mul_nonneg (NNReal.coe_nonneg _) (norm_nonneg _))
have hc₀ : c ≠ 0 := norm_pos_iff.1 (one_pos.trans hc)
rw [← h.1] at hc
rcases rescale_to_shell_zpow hc ε0 hx with ⟨n, -, hlt, -, hle⟩
simp only [← map_zpow₀, h.1, ← map_smulₛₗ] at hlt hle
calc
‖x‖ = ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ := by rwa [← norm_inv, ← norm_smul, inv_smul_smul₀ (zpow_ne_zero _ _)]
_ ≤ ‖c ^ n‖⁻¹ * 1 := by gcongr; exact (hε _ hlt).le
_ ≤ ε⁻¹ * ‖c‖ * ‖f x‖ := by rwa [mul_one]
