English
Let E and F be suitable topological groups (with a compatible linear structure) and let f: E →ₛₗ[σ] F be a semilinear map. If for every subset s ⊆ E that is Von Neumann bounded, the image f''s is Von Neumann bounded in F, then f is continuous at 0.
Русский
Пусть E и F — надлежаще заданные топологические группы с совместимой линейной структурой, и пусть f: E →ₛₗ[σ] F — полупрямой линейный отображение. Если для каждого подмножества s ⊆ E, являющегося ограниченным по Вон Неймену, образ f''s ограничен в F, то f непрерывно в 0.
LaTeX
$$$\forall s \subseteq E,\ IsVonNBounded_{\mathbb{k}}(s) \Rightarrow IsVonNBounded_{\mathbb{k}'}(f''s) \Rightarrow ContinuousAt\ f\ 0$$$
Lean4
theorem continuousAt_zero_of_locally_bounded (f : E →ₛₗ[σ] F)
(hf : ∀ s, IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (f '' s)) : ContinuousAt f 0 := by
-- Assume that f is not continuous at 0
by_contra h
rcases (nhds_basis_balanced 𝕜 E).exists_antitone_subbasis with ⟨b, bE1, bE⟩
simp only [_root_.id] at bE
have bE' : (𝓝 (0 : E)).HasBasis (fun x : ℕ => x ≠ 0) fun n : ℕ => (n : 𝕜)⁻¹ • b n :=
by
refine bE.1.to_hasBasis ?_ ?_
· intro n _
use n + 1
simp only [Ne, Nat.succ_ne_zero, not_false_iff, Nat.cast_add, Nat.cast_one, true_and]
-- `b (n + 1) ⊆ b n` follows from `Antitone`.
have h : b (n + 1) ⊆ b n := bE.2 (by simp)
refine _root_.trans ?_ h
rintro y
⟨x, hx, hy⟩
-- Since `b (n + 1)` is balanced `(n+1)⁻¹ b (n + 1) ⊆ b (n + 1)`
rw [← hy]
refine (bE1 (n + 1)).2.smul_mem ?_ hx
have h' : 0 < (n : ℝ) + 1 := n.cast_add_one_pos
rw [norm_inv, ← Nat.cast_one, ← Nat.cast_add, RCLike.norm_natCast, Nat.cast_add, Nat.cast_one,
inv_le_comm₀ h' zero_lt_one]
simp
intro n hn
have hcont : ContinuousAt (fun x : E => (n : 𝕜) • x) 0 := (continuous_const_smul (n : 𝕜)).continuousAt
simp only [ContinuousAt, smul_zero] at hcont
rw [bE.1.tendsto_left_iff] at hcont
rcases hcont (b n) (bE1 n).1 with ⟨i, _, hi⟩
refine ⟨i, trivial, fun x hx => ⟨(n : 𝕜) • x, hi hx, ?_⟩⟩
simp [← mul_smul, hn]
rw [ContinuousAt, map_zero, bE'.tendsto_iff (nhds_basis_balanced 𝕜' F)] at h
push_neg at h
rcases h with ⟨V, ⟨hV, -⟩, h⟩
simp only [_root_.id] at h
choose! u hu hu' using h
have h_tendsto : Tendsto (fun n : ℕ => (n : 𝕜) • u n) atTop (𝓝 (0 : E)) :=
by
apply bE.tendsto
intro n
by_cases h : n = 0
· rw [h, Nat.cast_zero, zero_smul]
exact mem_of_mem_nhds (bE.1.mem_of_mem <| by trivial)
rcases hu n h with ⟨y, hy, hu1⟩
convert hy
rw [← hu1, ← mul_smul]
simp only [h, mul_inv_cancel₀, Ne, Nat.cast_eq_zero, not_false_iff, one_smul]
-- The image `(fun n ↦ n • u n)` is von Neumann bounded:
have h_bounded : IsVonNBounded 𝕜 (Set.range fun n : ℕ => (n : 𝕜) • u n) :=
h_tendsto.cauchySeq.totallyBounded_range.isVonNBounded 𝕜
rcases (hf _ h_bounded hV).exists_pos with ⟨r, hr, h'⟩
obtain ⟨n, hn⟩ := exists_nat_gt r
have h1 : r ≤ ‖(n : 𝕜')‖ := by
rw [RCLike.norm_natCast]
exact hn.le
have hn' : 0 < ‖(n : 𝕜')‖ := lt_of_lt_of_le hr h1
rw [norm_pos_iff, Ne, Nat.cast_eq_zero] at hn'
have h'' : f (u n) ∈ V := by
simp only [Set.image_subset_iff] at h'
specialize h' (n : 𝕜') h1 (Set.mem_range_self n)
simp only [Set.mem_preimage, LinearMap.map_smulₛₗ, map_natCast] at h'
rcases h' with ⟨y, hy, h'⟩
apply_fun fun y : F => (n : 𝕜')⁻¹ • y at h'
simp only [hn', inv_smul_smul₀, Ne, Nat.cast_eq_zero, not_false_iff] at h'
rwa [← h']
exact hu' n hn' h''
