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

PL1/ALAtomic.lean

All source files · Download exact source

SHA-256: 2e0249914bd2ad4f2706d42106e2281aa7cf3e4fcc5b38d76dda3cc8617ee5a2

1import PL1.ALOrder2import PL1.AtomicBandDecomposition3import PL1.SchurApproximation45/-! # Actual scalar coordinates of atomic AL spaces -/67noncomputable section8open Filter TopologicalSpace9open scoped Topology BigOperators1011namespace PL1.ALAtomic12open AtomicBandDecomposition ALOrder1314variable {E : Type*} [NormedAddCommGroup E] [Lattice E]15  [IsOrderedAddMonoid E] [NormedVectorLattice E] [CompleteSpace E]16/-- A positive element of the principal band of an atom lies on its ray.17The proof uses norm convergence of its actual truncated principal-ideal net. -/18theorem mem_span_of_mem_atom_band_nonneg19    (hAL : ALRenorming.IsALNorm E) {a x : E} (ha : IsLatticeAtom a)20    (hx : 0 ≤ x) (hxa : x ∈ Band.generated ({a} : Set E)) :21    x ∈ Submodule.span ℝ ({a} : Set E) := by22  let y : ℕ → E := fun n => x ⊓ (n : ℝ) • a23  have hy : ∀ n, 0 ≤ y n := fun n =>24    le_inf hx (smul_nonneg (Nat.cast_nonneg _) ha.nonneg)25  have hmono : Monotone y := by26    intro m n hmn27    exact inf_le_inf_left _ (smul_le_smul_of_nonneg_right (Nat.cast_le.mpr hmn) ha.nonneg)28  obtain ⟨z, hz⟩ := ALOrder.exists_tendsto_of_monotone_net_norm_bounded hAL y hmono ‖x‖29    (fun n => norm_le_norm_of_abs_le_abs (by30      rw [abs_of_nonneg (hy n), abs_of_nonneg hx]31      exact inf_le_left))32  have hlub : IsLUB (Set.range y) x := by33    simpa only [y, Nat.cast_smul_eq_nsmul] using34      (Band.mem_generated_singleton_iff_isLUB_inf_nsmul ha.nonneg hx).mp hxa35  have hzx : z = x := (isLUB_of_tendsto_atTop hmono hz).unique hlub36  have hclosed := (Submodule.span ℝ ({a} : Set E)).closed_of_finiteDimensional37  apply hclosed.mem_of_tendsto (hz.trans (by rw [hzx]))38  exact Filter.Eventually.of_forall (fun n => by39    obtain ⟨t, _, ht⟩ := ha.eq_smul_of_nonneg_le_smul (hy n)40      (Nat.cast_nonneg n) (show y n ≤ (n : ℝ) • a from inf_le_right)41    rw [ht]42    exact Submodule.smul_mem _ t (Submodule.subset_span (Set.mem_singleton a)))4344/-- The principal band of an atom is exactly its one-dimensional real span. -/45theorem atom_band_eq_span (hAL : ALRenorming.IsALNorm E)46    {a : E} (ha : IsLatticeAtom a) :47    (Band.generated ({a} : Set E)).toSubmodule = Submodule.span ℝ ({a} : Set E) := by48  apply le_antisymm49  · intro x hx50    have hp := mem_span_of_mem_atom_band_nonneg hAL ha (posPart_nonneg x)51      ((Band.generated ({a} : Set E)).toOrderIdeal.posPart_mem hx)52    have hn := mem_span_of_mem_atom_band_nonneg hAL ha (negPart_nonneg x)53      ((Band.generated ({a} : Set E)).toOrderIdeal.negPart_mem hx)54    simpa only [posPart_sub_negPart] using (Submodule.span ℝ ({a} : Set E)).sub_mem hp hn55  · apply Submodule.span_le.mpr56    intro x hx57    exact Band.subset_generated _ hx585960theorem principalBand_submodule (hAL : ALRenorming.IsALNorm E)61    {a : E} (ha : IsLatticeAtom a) :62    (ALOrder.principalBand hAL a).toSubmodule = Submodule.span ℝ ({a} : Set E) := by63  have heq : (ALOrder.principalBand hAL a).toSubmodule =64      (Band.generated ({a} : Set E)).toSubmodule :=65    SetLike.coe_injective (ALOrder.principalBand_coe hAL a)66  exact heq.trans (atom_band_eq_span hAL ha)6768variable [TopologicalSpace.SeparableSpace E]6970private instance atomsCountable : Countable (normalizedLatticeAtoms E) :=71  normalizedLatticeAtoms_countable.to_subtype7273private noncomputable instance atomsEncodable : Encodable (normalizedLatticeAtoms E) :=74  Encodable.ofCountable _7576/-- Each normalized atom is listed exactly once; unused indices carry the zero band. -/77def atomBand (hAL : ALRenorming.IsALNorm E) (n : ℕ) : ProjectionBand E :=78  (Encodable.decode₂ (normalizedLatticeAtoms E) n).elim ⊥79    (fun a => ALOrder.principalBand hAL a)8081def atomProjection (hAL : ALRenorming.IsALNorm E) (n : ℕ) : E →L[ℝ] E :=82  projection (atomBand hAL n)8384theorem atomProjection_eq_smul (hAL : ALRenorming.IsALNorm E) (n : ℕ) (x : E)85    {a : normalizedLatticeAtoms E}86    (ha : Encodable.decode₂ (normalizedLatticeAtoms E) n = some a) :87    ∃ t : ℝ, atomProjection hAL n x = t • (a : E) := by88  have hm := projection_mem (atomBand hAL n) x89  change atomProjection hAL n x ∈ (atomBand hAL n).toSubmodule at hm90  rw [show atomBand hAL n = ALOrder.principalBand hAL a by simp [atomBand, ha],91    principalBand_submodule hAL a.property.1] at hm92  obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hm93  exact ⟨t, ht.symm⟩9495theorem atomProjection_eq_zero (hAL : ALRenorming.IsALNorm E) (n : ℕ) (x : E)96    (ha : Encodable.decode₂ (normalizedLatticeAtoms E) n = none) :97    atomProjection hAL n x = 0 := by98  have hm := projection_mem (atomBand hAL n) x99  change atomProjection hAL n x ∈ (atomBand hAL n).toSubmodule at hm100  rw [show atomBand hAL n = ⊥ by simp [atomBand, ha]] at hm101  exact hm102103theorem atomProjection_pairwise (hAL : ALRenorming.IsALNorm E) (x y : E) :104    Pairwise (fun m n => IsVLDisjoint (atomProjection hAL m x) (atomProjection hAL n y)) := by105  intro m n hmn106  cases hm : Encodable.decode₂ (normalizedLatticeAtoms E) m with107  | none => rw [atomProjection_eq_zero hAL m x hm]; exact isVLDisjoint_zero_left _108  | some a =>109    cases hn : Encodable.decode₂ (normalizedLatticeAtoms E) n with110    | none => rw [atomProjection_eq_zero hAL n y hn]; exact isVLDisjoint_zero_right _111    | some b =>112      have hab : (a : E) ≠ (b : E) := by113        intro heq114        have hsub : a = b := Subtype.ext heq115        exact hmn ((Encodable.decode₂_eq_some.mp hm).symm.trans116          (hsub ▸ Encodable.decode₂_eq_some.mp hn))117      obtain ⟨s, hs⟩ := atomProjection_eq_smul hAL m x hm118      obtain ⟨t, ht⟩ := atomProjection_eq_smul hAL n y hn119      rw [hs, ht]120      exact ((a.property.1.isVLDisjoint_of_norm_eq_one b.property.1121        a.property.2 b.property.2 hab).smul_left s).smul_right t122123def coordinate (hAL : ALRenorming.IsALNorm E) (n : ℕ) : E →L[ℝ] ℝ :=124  (normFunctional hAL).comp (atomProjection hAL n)125126theorem norm_coordinate (hAL : ALRenorming.IsALNorm E) (n : ℕ) (x : E) :127    ‖coordinate hAL n x‖ = ‖atomProjection hAL n x‖ := by128  change ‖normFunctional hAL (atomProjection hAL n x)‖ = _129  cases hn : Encodable.decode₂ (normalizedLatticeAtoms E) n with130  | none => simp [atomProjection_eq_zero hAL n x hn]131  | some a =>132    obtain ⟨t, ht⟩ := atomProjection_eq_smul hAL n x hn133    rw [ht, map_smul, norm_smul, norm_smul,134      normFunctional_nonneg hAL a.property.1.nonneg]135    simp only [norm_norm]136137theorem sum_atomProjection_le (hAL : ALRenorming.IsALNorm E)138    {x : E} (hx : 0 ≤ x) (N : ℕ) :139    (∑ n ∈ Finset.range N, atomProjection hAL n x) ≤ x := by140  by_cases hN : N = 0141  · simpa [hN] using hx142  rw [← Fin.sum_univ_eq_sum_range (fun n => atomProjection hAL n x)]143  have hp (i : Fin N) : 0 ≤ atomProjection hAL i x := projection_nonneg _ hx144  rw [sum_eq_sup_of_pairwise_isVLDisjoint_of_nonneg (Nat.pos_of_ne_zero hN)145    hp146    (fun i j hij => atomProjection_pairwise hAL x x (fun h => hij (Fin.ext h)))]147  exact Finset.sup'_le _ _ (fun i _ => projection_le_self (atomBand hAL i) hx)148149omit [NormedVectorLattice E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] in150theorem norm_sum_nonneg (hAL : ALRenorming.IsALNorm E) {ι : Type*}151    (s : Finset ι) (x : ι → E) (hx : ∀ i ∈ s, 0 ≤ x i) :152    ‖∑ i ∈ s, x i‖ = ∑ i ∈ s, ‖x i‖ := by153  classical154  induction s using Finset.induction_on with155  | empty => simp156  | @insert i s hi ih =>157    rw [Finset.sum_insert hi, Finset.sum_insert hi,158      hAL _ _ (hx i (Finset.mem_insert_self i s))159        (Finset.sum_nonneg fun j hj => hx j (Finset.mem_insert_of_mem hj))]160    rw [ih (fun j hj => hx j (Finset.mem_insert_of_mem hj))]161162theorem sum_norm_atomProjection_le (hAL : ALRenorming.IsALNorm E) (x : E) (N : ℕ) :163    (∑ n ∈ Finset.range N, ‖atomProjection hAL n x‖) ≤ ‖x‖ := by164  have hp (n : ℕ) : |atomProjection hAL n x| ≤ atomProjection hAL n |x| :=165    Positive.abs_le_map_abs (fun y hy => projection_nonneg (atomBand hAL n) hy) x166  calc167    ∑ n ∈ Finset.range N, ‖atomProjection hAL n x‖ ≤168        ∑ n ∈ Finset.range N, ‖atomProjection hAL n |x|‖ := by169      apply Finset.sum_le_sum170      intro n _171      exact norm_le_norm_of_abs_le_abs ((hp n).trans (le_abs_self _))172    _ = ‖∑ n ∈ Finset.range N, atomProjection hAL n |x|‖ :=173      (norm_sum_nonneg hAL _ _ (fun n _ => projection_nonneg _ (abs_nonneg x))).symm174    _ ≤ ‖x‖ := norm_le_norm_of_abs_le_abs (by175      have hpos : 0 ≤ ∑ n ∈ Finset.range N, atomProjection hAL n |x| :=176        Finset.sum_nonneg fun n _ => projection_nonneg _ (abs_nonneg x)177      rw [abs_of_nonneg hpos]178      exact sum_atomProjection_le hAL (abs_nonneg x) N)179180theorem summable_norm_atomProjection (hAL : ALRenorming.IsALNorm E) (x : E) :181    Summable (fun n => ‖atomProjection hAL n x‖) :=182  summable_of_sum_range_le (fun _ => norm_nonneg _) (sum_norm_atomProjection_le hAL x)183184theorem atomBand_cover (hAL : ALRenorming.IsALNorm E) {a : E} (ha : IsLatticeAtom a) :185    ∃ n, a ∈ atomBand hAL n := by186  let b : normalizedLatticeAtoms E := ⟨‖a‖⁻¹ • a, ha.normalize, ha.norm_normalize⟩187  refine ⟨Encodable.encode b, ?_⟩188  have hb : atomBand hAL (Encodable.encode b) = ALOrder.principalBand hAL b := by189    simp [atomBand, Encodable.decode₂_encode]190  rw [hb]191  have hm := (ALOrder.principalBand hAL b).toSubmodule.smul_mem ‖a‖192    (ALOrder.mem_principalBand_self hAL b)193  change a ∈ (ALOrder.principalBand hAL b).toSubmodule194  simpa only [b, smul_inv_smul₀ (norm_ne_zero_iff.mpr ha.ne_zero)] using hm195196/-- Atomicity forces the actual positive atom projections to exhaust each vector. -/197theorem tendsto_sum_atomProjection (hAL : ALRenorming.IsALNorm E) (hA : IsAtomicLattice E)198    (x : E) :199    Tendsto (fun N => ∑ n ∈ Finset.range N, atomProjection hAL n x) atTop (𝓝 x) := by200  have hpos (x : E) (hx : 0 ≤ x) :201      Tendsto (fun N => ∑ n ∈ Finset.range N, atomProjection hAL n x) atTop (𝓝 x) := by202    let z := ∑' n, atomProjection hAL n x203    have ht : Tendsto (fun N => ∑ n ∈ Finset.range N, atomProjection hAL n x)204        atTop (𝓝 z) := (summable_norm_atomProjection hAL x).of_norm.hasSum.tendsto_sum_nat205    have hzx : z ≤ x := le_of_tendsto' ht (sum_atomProjection_le hAL hx)206    have hnp (n : ℕ) : atomProjection hAL n x ≤ z := by207      have hm : Monotone (fun N => ∑ n ∈ Finset.range N, atomProjection hAL n x) := by208        apply monotone_nat_of_le_succ209        intro N210        rw [Finset.sum_range_succ]211        exact le_add_of_nonneg_right (projection_nonneg _ hx)212      have hn : atomProjection hAL n x ≤213          ∑ j ∈ Finset.range (n + 1), atomProjection hAL j x :=214        Finset.single_le_sum (fun j _ => projection_nonneg _ hx) (Finset.mem_range.mpr (Nat.lt_succ_self n))215      exact hn.trans ((isLUB_of_tendsto_atTop hm ht).1 (Set.mem_range_self (n + 1)))216    have heq : z = x := by217      by_contra hne218      have hr : 0 < x - z := lt_of_le_of_ne (sub_nonneg.mpr hzx)219        (fun he => hne (sub_eq_zero.mp he.symm).symm)220      obtain ⟨a, ha, har⟩ := hA _ hr221      obtain ⟨n, han⟩ := atomBand_cover hAL ha222      have hbound : a ≤ x - atomProjection hAL n x :=223        har.trans (sub_le_sub_left (hnp n) x)224      have had : a ∈ disjointComplement (atomBand hAL n : Set E) :=225        (Band.disjointComplement (atomBand hAL n : Set E)).solid226          ((atomBand hAL n).id_sub_bandProjection_mem x) ha.nonneg hbound227      exact ha.ne_zero (Set.mem_singleton_iff.mp228        (disjointComplement_inter_eq_zero _ ⟨han, had⟩))229    exact heq ▸ ht230  have hp := hpos x⁺ (posPart_nonneg x)231  have hn := hpos x⁻ (negPart_nonneg x)232  simpa only [← Finset.sum_sub_distrib, ← map_sub, posPart_sub_negPart] using hp.sub hn233234theorem tsum_atomProjection (hAL : ALRenorming.IsALNorm E) (hA : IsAtomicLattice E)235    (x : E) : (∑' n, atomProjection hAL n x) = x :=236  tendsto_nhds_unique (summable_norm_atomProjection hAL x).of_norm.hasSum.tendsto_sum_nat237    (tendsto_sum_atomProjection hAL hA x)238239theorem summable_norm_coordinate (hAL : ALRenorming.IsALNorm E) (x : E) :240    Summable (fun n => ‖coordinate hAL n x‖) := by241  simpa only [norm_coordinate] using summable_norm_atomProjection hAL x242243def coordinateLinear (hAL : ALRenorming.IsALNorm E) : E →ₗ[ℝ] Ell1 ℝ where244  toFun x := ⟨fun n => coordinate hAL n x, memℓp_gen (by simpa using summable_norm_coordinate hAL x)⟩245  map_add' x y := by apply lp.ext; funext n; exact map_add (coordinate hAL n) x y246  map_smul' c x := by apply lp.ext; funext n; exact map_smul (coordinate hAL n) c x247248theorem norm_coordinateLinear_le (hAL : ALRenorming.IsALNorm E) (x : E) :249    ‖coordinateLinear hAL x‖ ≤ ‖x‖ := by250  rw [L1Sum.norm_eq_tsum]251  change (∑' n, ‖coordinate hAL n x‖) ≤ ‖x‖252  simp_rw [norm_coordinate]253  exact le_of_tendsto' (summable_norm_atomProjection hAL x).hasSum.tendsto_sum_nat254    (sum_norm_atomProjection_le hAL x)255256theorem norm_coordinateLinear (hAL : ALRenorming.IsALNorm E) (hA : IsAtomicLattice E)257    (x : E) : ‖coordinateLinear hAL x‖ = ‖x‖ := by258  refine le_antisymm (norm_coordinateLinear_le hAL x) ?_259  rw [L1Sum.norm_eq_tsum]260  change ‖x‖ ≤ ∑' n, ‖coordinate hAL n x‖261  simp_rw [norm_coordinate]262  have h := norm_tsum_le_tsum_norm (summable_norm_atomProjection hAL x)263  rwa [tsum_atomProjection hAL hA x] at h264265/-- The actual scalar atom coordinates form an isometric embedding into ℓ₁. -/266def coordinateIsometry (hAL : ALRenorming.IsALNorm E) (hA : IsAtomicLattice E) :267    E →ₗᵢ[ℝ] Ell1 ℝ :=268  { coordinateLinear hAL with norm_map' := norm_coordinateLinear hAL hA }269270theorem containsIsomorphicCopy_ell1 (hAL : ALRenorming.IsALNorm E)271    (hA : IsAtomicLattice E) : ContainsIsomorphicCopy ℝ E (Ell1 ℝ) := by272  let J := (coordinateIsometry hAL hA).toContinuousLinearMap273  have hJ : Topology.IsClosedEmbedding J := (coordinateIsometry hAL hA).isometry.isClosedEmbedding274  exact ⟨J.range, hJ.isClosed_range, ⟨J.equivRange hJ.injective hJ.isClosed_range⟩⟩275276/-- A separable atomic complete AL space has the Schur property. -/277theorem hasSchurProperty (hAL : ALRenorming.IsALNorm E) (hA : IsAtomicLattice E) :278    HasSchurProperty ℝ E :=279  (ell1_hasSchurProperty ℝ).of_containsIsomorphicCopy (containsIsomorphicCopy_ell1 hAL hA)280281end PL1.ALAtomic282283