On complemented subspaces of L1[0,1]L_1[0,1]

PL1/ALOrder.lean

All source files · Download exact source

SHA-256: b73962efa0f9192a78a0e08256218d2c042fd5b7685f7d6707d7c8bf81d4906b

1import PL1.ALRenorming2import PL1.LatticeStrictPositive3import BanLat.Substructures.Band.PPP45/-!6# Monotone completeness from an AL norm78Positive additivity alone supplies the norming positive functional and norm9convergence of bounded monotone nets. No Schur-property premise is used.10-/1112noncomputable section13open Filter14open scoped Topology1516namespace PL1.ALOrder1718open ALRenorming1920variable {E : Type*} [NormedAddCommGroup E] [Lattice E]21  [IsOrderedAddMonoid E] [NormedVectorLattice E]2223def normLinear (hAL : IsALNorm E) : E →ₗ[ℝ] ℝ :=24  Positive.extension (fun x _ => norm_nonneg x) hAL2526theorem normLinear_nonneg (hAL : IsALNorm E) {x : E} (hx : 0 ≤ x) :27    normLinear hAL x = ‖x‖ := Positive.extension_nonneg _ _ hx2829theorem normLinear_positive (hAL : IsALNorm E) : Positive (normLinear hAL) :=30  Positive.extension_positive _ _3132theorem abs_normLinear_le (hAL : IsALNorm E) (x : E) : |normLinear hAL x| ≤ ‖x‖ := by33  have h := Positive.abs_le_map_abs (normLinear_positive hAL) x34  rwa [normLinear_nonneg hAL (abs_nonneg x), norm_abs_eq_norm] at h3536/-- The positive functional whose value on every positive vector is its norm. -/37def normFunctional (hAL : IsALNorm E) : E →L[ℝ] ℝ :=38  (normLinear hAL).mkContinuous 1 (fun x => by39    simpa only [Real.norm_eq_abs, one_mul] using abs_normLinear_le hAL x)4041@[simp] theorem normFunctional_nonneg (hAL : IsALNorm E) {x : E} (hx : 0 ≤ x) :42    normFunctional hAL x = ‖x‖ := normLinear_nonneg hAL hx4344theorem normFunctional_strictlyPositive (hAL : IsALNorm E) :45    SchurLattice.IsStrictlyPositive (normFunctional hAL) := by46  intro x hx47  rw [normFunctional_nonneg hAL hx.le]48  exact norm_pos_iff.mpr (ne_of_gt hx)4950theorem norm_sub_of_le (hAL : IsALNorm E) {x y : E} (hxy : x ≤ y) :51    ‖y - x‖ = normFunctional hAL y - normFunctional hAL x := by52  rw [← map_sub, normFunctional_nonneg hAL (sub_nonneg.mpr hxy)]5354private theorem cauchy_map_atTop_of_near_base {ι Y : Type*}55    [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] [PseudoMetricSpace Y]56    (x : ι → Y)57    (h : ∀ ε : ℝ, 0 < ε → ∃ i, ∀ j, i ≤ j → dist (x j) (x i) < ε) :58    Cauchy (Filter.map x atTop) := by59  rw [Metric.cauchy_iff]60  refine ⟨inferInstance, fun ε hε => ?_⟩61  obtain ⟨i, hi⟩ := h (ε / 2) (half_pos hε)62  refine ⟨x '' Set.Ici i, Filter.image_mem_map (Ici_mem_atTop i), ?_⟩63  rintro _ ⟨j, hj, rfl⟩ _ ⟨k, hk, rfl⟩64  have hj' := hi j hj65  have hk' := hi k hk66  have ht := dist_triangle (x j) (x i) (x k)67  rw [dist_comm (x i) (x k)] at ht68  linarith6970/-- Every norm-bounded monotone directed net converges in a complete AL space. -/71theorem exists_tendsto_of_monotone_net_norm_bounded [CompleteSpace E]72    {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]73    (hAL : IsALNorm E) (x : ι → E) (hmono : Monotone x)74    (M : ℝ) (hM : ∀ i, ‖x i‖ ≤ M) : ∃ a : E, Tendsto x atTop (𝓝 a) := by75  let f : ι → ℝ := fun i => normFunctional hAL (x i)76  have hm : Monotone f := (Positive.monotone_iff.mpr (normLinear_positive hAL)).comp hmono77  have hb : BddAbove (Set.range f) := ⟨M, by78    rintro _ ⟨i, rfl⟩79    exact (le_abs_self (f i)).trans ((abs_normLinear_le hAL (x i)).trans (hM i))⟩80  have ht : Tendsto f atTop (𝓝 (⨆ i, f i)) := tendsto_atTop_ciSup hm hb81  apply cauchy_map_iff_exists_tendsto.mp82  apply cauchy_map_atTop_of_near_base83  intro ε hε84  have he : ∀ᶠ i in atTop, dist (f i) (⨆ j, f j) < ε / 2 :=85    (Metric.tendsto_nhds.mp ht) _ (half_pos hε)86  obtain ⟨i, hi⟩ := eventually_atTop.1 he87  refine ⟨i, fun j hij => ?_⟩88  have hd : dist (f j) (f i) < ε := by89    have hh := dist_triangle (f j) (⨆ k, f k) (f i)90    rw [dist_comm (⨆ k, f k) (f i)] at hh91    linarith [hi j hij, hi i le_rfl]92  rw [dist_eq_norm, norm_sub_of_le hAL (hmono hij)]93  exact (le_abs_self _).trans_lt (by simpa only [Real.dist_eq] using hd)9495theorem exists_tendsto_of_antitone_net_norm_bounded [CompleteSpace E]96    {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]97    (hAL : IsALNorm E) (x : ι → E) (hanti : Antitone x)98    (M : ℝ) (hM : ∀ i, ‖x i‖ ≤ M) : ∃ a : E, Tendsto x atTop (𝓝 a) := by99  obtain ⟨a, ha⟩ := exists_tendsto_of_monotone_net_norm_bounded hAL (fun i => -x i)100    (fun i j hij => neg_le_neg (hanti hij)) M (fun i => by simpa using hM i)101  exact ⟨-a, by simpa only [neg_neg] using ha.neg⟩102103/-- The actual existing order of a complete AL space is Dedekind complete. -/104@[reducible] def conditionallyCompleteLattice [CompleteSpace E] (hAL : IsALNorm E) :105    ConditionallyCompleteLattice E :=106  conditionallyCompleteLatticeOfPosNet E (by107    intro ι _ _ _ x hmono hx hbdd108    obtain ⟨b, hb⟩ := hbdd109    obtain ⟨a, ha⟩ := exists_tendsto_of_monotone_net_norm_bounded hAL x hmono ‖b‖ (by110      intro i111      apply norm_le_norm_of_abs_le_abs112      rw [abs_of_nonneg (hx i)]113      exact (hb (Set.mem_range_self i)).trans (le_abs_self b))114    exact ⟨a, isLUB_of_tendsto_atTop hmono ha⟩)115116theorem conditionallyCompleteLattice_toLattice [CompleteSpace E] (hAL : IsALNorm E) :117    (conditionallyCompleteLattice hAL).toLattice = (inferInstance : Lattice E) := rfl118119theorem exists_isLUB [CompleteSpace E] (hAL : IsALNorm E)120    (s : Set E) (hne : s.Nonempty) (hbdd : BddAbove s) : ∃ a, IsLUB s a := by121  let := conditionallyCompleteLattice hAL122  exact ⟨sSup s, isLUB_csSup hne hbdd⟩123124theorem tendsto_zero_of_antitone_net_isGLB [CompleteSpace E]125    {ι : Type*} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]126    (hAL : IsALNorm E) (x : ι → E) (hanti : Antitone x)127    (hglb : IsGLB (Set.range x) 0) : Tendsto x atTop (𝓝 0) := by128  classical129  let i₀ : ι := Classical.choice ‹Nonempty ι›130  let : Nonempty (Set.Ici i₀) := ⟨⟨i₀, le_rfl⟩⟩131  let : IsDirectedOrder (Set.Ici i₀) := ⟨fun i j => by132    obtain ⟨k, hik, hjk⟩ := exists_ge_ge (i : ι) (j : ι)133    exact ⟨⟨k, i.prop.trans hik⟩, hik, hjk⟩⟩134  let y : Set.Ici i₀ → E := fun i => x i135  have hy : Antitone y := fun i j hij => hanti hij136  have hx : ∀ i, 0 ≤ x i := fun i => hglb.1 (Set.mem_range_self i)137  obtain ⟨a, ha⟩ := exists_tendsto_of_antitone_net_norm_bounded hAL y hy ‖x i₀‖ (by138    intro i139    apply norm_le_norm_of_abs_le_abs140    simpa only [y, abs_of_nonneg (hx i), abs_of_nonneg (hx i₀)] using hanti i.prop)141  have htail : Tendsto x atTop (𝓝 a) := tendsto_comp_val_Ici_atTop.mp ha142  have heq : a = 0 := (isGLB_of_tendsto_atTop hanti htail).unique hglb143  exact heq ▸ htail144145/-- An actual projection band for a prescribed band of the original lattice. -/146def bandOfAL [CompleteSpace E] (hAL : IsALNorm E) (B : Band E) : ProjectionBand E :=147  Classical.choose ((ProjectionBand.projectionBand_iff_isLUB_inter_Icc B).mpr (by148    intro x hx149    exact exists_isLUB hAL _150      ⟨0, B.toSubmodule.zero_mem, le_rfl, hx⟩ ⟨x, fun _ hy => hy.2.2⟩))151152theorem bandOfAL_coe [CompleteSpace E] (hAL : IsALNorm E) (B : Band E) :153    (bandOfAL hAL B : Set E) = (B : Set E) :=154  Classical.choose_spec ((ProjectionBand.projectionBand_iff_isLUB_inter_Icc B).mpr (by155    intro x hx156    exact exists_isLUB hAL _157      ⟨0, B.toSubmodule.zero_mem, le_rfl, hx⟩ ⟨x, fun _ hy => hy.2.2⟩))158159def principalBand [CompleteSpace E] (hAL : IsALNorm E) (a : E) : ProjectionBand E :=160  bandOfAL hAL (Band.generated ({a} : Set E))161162theorem principalBand_coe [CompleteSpace E] (hAL : IsALNorm E) (a : E) :163    (principalBand hAL a : Set E) = (Band.generated ({a} : Set E) : Set E) :=164  bandOfAL_coe hAL _165166theorem mem_principalBand_self [CompleteSpace E] (hAL : IsALNorm E) (a : E) :167    a ∈ principalBand hAL a := by168  change a ∈ (principalBand hAL a : Set E)169  rw [principalBand_coe]170  exact Band.subset_generated _ (Set.mem_singleton a)171172end PL1.ALOrder173