PL1/SchurLatticeCompactness.lean

All source files · Download exact source

SHA-256: 6269e57eb4fe6db954f5cd32540c4407e28f41419b3527acecc1351e2abf61a8

1import PL1.SchurLattice2import Mathlib.Analysis.Normed.Module.HahnBanach3import Mathlib.Analysis.Normed.Module.WeakDual45/-!6# Weak compactness in separable Schur spaces78These lemmas prove the norm-compactness consequence of weak compactness,9without assuming that the continuous dual is separable. Weak compactness of10order intervals is a separate premise in the lattice corollary below.11-/1213noncomputable section14open Filter TopologicalSpace15open scoped Topology1617namespace PL1.SchurLattice1819variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]20  [SeparableSpace E]2122/-- Hahn--Banach applied to a norm-dense sequence gives a countable family23of continuous functionals separating every pair of points. The dual space24itself need not be separable. -/25theorem exists_countable_separating_dual :26    ∃ g : ℕ → E →L[𝕜] 𝕜, (∀ n, ‖g n‖ ≤ 1) ∧27      ∀ ⦃x y : E⦄, x ≠ y → ∃ n, g n x ≠ g n y := by28  classical29  choose g hg hgn using fun n => exists_dual_vector'' 𝕜 (denseSeq E n)30  refine ⟨g, hg, ?_⟩31  intro x y hxy32  by_contra hbad33  push Not at hbad34  let z := x - y35  have hz : z ≠ 0 := sub_ne_zero.mpr hxy36  have hgz (n : ℕ) : g n z = 0 := by simp [z, hbad n]37  obtain ⟨n, hn⟩ := (denseRange_denseSeq E).exists_dist_lt z38    (show 0 < ‖z‖ / 3 from div_pos (norm_pos_iff.mpr hz) (by norm_num))39  have hdist : ‖z - denseSeq E n‖ < ‖z‖ / 3 := by simpa [dist_eq_norm] using hn40  have hgnorm : ‖denseSeq E n‖ ≤ ‖z - denseSeq E n‖ := by41    have hb := (g n).le_opNorm (z - denseSeq E n)42    rw [map_sub, hgz, hgn] at hb43    simpa using hb.trans (mul_le_of_le_one_left (norm_nonneg _) (hg n))44  have hzbound : ‖z‖ ≤ ‖z - denseSeq E n‖ + ‖denseSeq E n‖ := by45    simpa only [sub_add_cancel] using norm_add_le (z - denseSeq E n) (denseSeq E n)46  linarith [norm_nonneg z]4748/-- Every weakly compact subset of a separable normed space is metrizable in49its weak topology. This is restricted to compact subsets. -/50theorem weak_metrizable_of_isCompact (K : Set (WeakSpace 𝕜 E))51    (hK : IsCompact K) : MetrizableSpace K := by52  let : CompactSpace K := isCompact_iff_compactSpace.mp hK53  obtain ⟨g, _, hsep⟩ := exists_countable_separating_dual (𝕜 := 𝕜) (E := E)54  apply Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating55    (fun n (x : K) => g n ((toWeakSpace 𝕜 E).symm x.val))56  · intro n57    exact (WeakBilin.eval_continuous (topDualPairing 𝕜 E).flip (g n)).comp58      continuous_subtype_val59  · intro x y hxy60    exact hsep (fun h => hxy (Subtype.ext ((toWeakSpace 𝕜 E).symm.injective h)))6162/-- Weak compactness implies weak sequential compactness for subsets of a63separable normed space; no general Eberlein--Smulian theorem is used. -/64theorem weak_isSeqCompact_of_isCompact (K : Set (WeakSpace 𝕜 E))65    (hK : IsCompact K) : IsSeqCompact K := by66  let : CompactSpace K := isCompact_iff_compactSpace.mp hK67  let : MetrizableSpace K := weak_metrizable_of_isCompact K hK68  simpa using IsSeqCompact.range69    (continuous_iff_seqContinuous.mp (continuous_subtype_val : Continuous70      (fun x : K => (x : WeakSpace 𝕜 E))))7172/-- A weakly compact set in a separable Schur space is compact for the73original norm topology. -/74theorem isCompact_of_weak_isCompact (hS : HasSchurProperty 𝕜 E)75    (s : Set E) (hs : IsCompact ((toWeakSpace 𝕜 E) '' s)) : IsCompact s := by76  apply IsSeqCompact.isCompact77  intro x hx78  obtain ⟨a, ha, φ, hφ, hlim⟩ := weak_isSeqCompact_of_isCompact _ hs79    (fun n => Set.mem_image_of_mem _ (hx n))80  obtain ⟨a, ha, rfl⟩ := ha81  refine ⟨a, ha, φ, hφ, hS _ _ ?_⟩82  intro g83  exact ((WeakBilin.eval_continuous (topDualPairing 𝕜 E).flip g).tendsto _).comp hlim8485/-- On subsets of a separable Schur space, weak compactness and norm86compactness agree. -/87theorem isCompact_iff_weak_isCompact (hS : HasSchurProperty 𝕜 E) (s : Set E) :88    IsCompact s ↔ IsCompact ((toWeakSpace 𝕜 E) '' s) :=89  ⟨fun hs => hs.image (toWeakSpaceCLM 𝕜 E).continuous,90    isCompact_of_weak_isCompact hS s⟩9192end PL1.SchurLattice93