PL1/SeparableRange.lean

All source files · Download exact source

SHA-256: d4925c6faf4d559dc498fdd880b29259db4b72db64cd32a2a8e2a52dd920a866

1import PL1.RealSchur23/-! # Separability of the concrete projection ranges -/45noncomputable section6open Filter Set TopologicalSpace7open scoped Topology ENNReal NNReal89namespace PL11011variable (𝕜 : Type*) [RCLike 𝕜]1213/-- A countable ell1 sum of a separable normed space is separable. -/14theorem L1Sum.separableSpace (Y : Type*) [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]15    [SeparableSpace Y] : SeparableSpace (L1Sum Y) := by16  classical17  let A : Set (L1Sum Y) := ⋃ n : ℕ, range (lp.single (E := fun _ : ℕ => Y) 1 n)18  let M : Submodule 𝕜 (L1Sum Y) := Submodule.span 𝕜 A19  have hsep : IsSeparable A := by20    apply IsSeparable.iUnion21    intro n22    exact isSeparable_range (lp.singleContinuousLinearMap 𝕜 (fun _ : ℕ => Y) 1 n).continuous23  have hdense : Dense (M : Set (L1Sum Y)) := by24    intro f25    apply isClosed_closure.mem_of_tendsto (lp.hasSum_single (by simp) f)26    apply Eventually.of_forall27    intro s28    apply subset_closure29    apply M.sum_mem30    intro n _31    exact Submodule.subset_span (mem_iUnion.mpr ⟨n, ⟨f n, rfl⟩⟩)32  apply isSeparable_univ_iff.mp33  rw [← hdense.closure_eq]34  exact hsep.span.closure3536/-- The countable Walsh span supplies separability of the actual Haar L1 space. -/37theorem Walsh.separableSpace_scalarL1 :38    SeparableSpace (MeasureTheory.Lp 𝕜 1 Walsh.haar) := by39  apply isSeparable_univ_iff.mp40  rw [← (Walsh.dense_span_scalarCharacterLp 𝕜 1 (by norm_num)).closure_eq]41  exact (countable_range (Walsh.scalarCharacterLp 𝕜 1)).isSeparable.span.closure4243theorem Noise.projection_range_separableSpace (rates : ℕ → ℝ≥0) :44    SeparableSpace (Noise.projection 𝕜 rates).range := by45  let : SeparableSpace (MeasureTheory.Lp 𝕜 1 Walsh.haar) := Walsh.separableSpace_scalarL1 𝕜46  let : SeparableSpace (L1Sum (MeasureTheory.Lp 𝕜 1 Walsh.haar)) := L1Sum.separableSpace 𝕜 _47  have := UniformSpace.secondCountable_of_separable (L1Sum (MeasureTheory.Lp 𝕜 1 Walsh.haar))48  infer_instance4950theorem Noise.projection_range_underlyingReal_separableSpace (rates : ℕ → ℝ≥0) :51    SeparableSpace (UnderlyingReal 𝕜 (Noise.projection 𝕜 rates).range) :=52  Noise.projection_range_separableSpace 𝕜 rates5354end PL155