PL1/AtomicBandDecomposition.lean
All source files · Download exact source
SHA-256: 3763c67c735d58a4fca1eef0cf7f91f0f5fc2c1223a1a038a138ec2631716b3c
1import PL1.LatticeAtoms2import PL1.UnconditionalRNP3import BanLat.Substructures.Band.PPP45/-!6# Atomic band projections in Schur Banach lattices78All projections in this module use the given BanLat order and norm. Atomicity9is a stated hypothesis, not a consequence supplied by the imported library.10-/1112noncomputable section13open Filter14open scoped Topology BigOperators15universe u v1617namespace PL1.AtomicBandDecomposition1819variable {E : Type u} [NormedAddCommGroup E] [Lattice E]20 [IsOrderedAddMonoid E] [NormedVectorLattice E]2122/-- Every band projection is contractive for the original lattice norm. -/23theorem norm_bandProjection_le (B : ProjectionBand E) (x : E) :24 ‖B.bandProjection x‖ ≤ ‖x‖ := by25 apply norm_le_norm_of_abs_le_abs26 exact (Positive.abs_le_map_abs (Positive.zero_le_iff.mp B.bandProjection_nonneg) x).trans27 (Positive.le_iff.mp B.bandProjection_le_id _ (abs_nonneg x))2829/-- The actual continuous linear operator associated with a projection band. -/30def projection (B : ProjectionBand E) : E →L[ℝ] E :=31 B.bandProjection.mkContinuous 1 (fun x => by32 simpa only [one_mul] using norm_bandProjection_le B x)3334@[simp] theorem projection_apply (B : ProjectionBand E) (x : E) :35 projection B x = B.bandProjection x := rfl3637theorem norm_projection_le (B : ProjectionBand E) : ‖projection B‖ ≤ 1 :=38 ContinuousLinearMap.opNorm_le_bound _ zero_le_one (fun x => by39 simpa only [one_mul, projection_apply] using norm_bandProjection_le B x)4041theorem projection_nonneg (B : ProjectionBand E) {x : E} (hx : 0 ≤ x) :42 0 ≤ projection B x := Positive.zero_le_iff.mp B.bandProjection_nonneg x hx4344theorem projection_le_self (B : ProjectionBand E) {x : E} (hx : 0 ≤ x) :45 projection B x ≤ x := Positive.le_iff.mp B.bandProjection_le_id x hx4647theorem projection_mem (B : ProjectionBand E) (x : E) : projection B x ∈ B :=48 B.bandProjection_mem x4950theorem projection_eq_self (B : ProjectionBand E) {x : E} (hx : x ∈ B) :51 projection B x = x := B.bandProjection_eq_of_mem hx5253theorem projection_eq_zero (B : ProjectionBand E) {x : E}54 (hx : x ∈ disjointComplement (B : Set E)) : projection B x = 0 :=55 B.bandProjection_eq_zero_of_mem_dc hx5657@[simp] theorem projection_bot : projection (⊥ : ProjectionBand E) = 0 := by58 ext x59 exact ProjectionBand.mem_bot.mp (projection_mem ⊥ x)6061theorem projection_comp (B C : ProjectionBand E) :62 (projection B).comp (projection C) = projection (B ⊓ C) := by63 ext x64 exact (LinearMap.congr_fun (ProjectionBand.bandProjection_inf B C) x).symm6566theorem projection_comp_of_le {B C : ProjectionBand E} (hBC : B ≤ C) :67 (projection B).comp (projection C) = projection B := by68 rw [projection_comp, inf_eq_left.mpr hBC]6970theorem projection_mono {B C : ProjectionBand E} (hBC : B ≤ C)71 {x : E} (hx : 0 ≤ x) : projection B x ≤ projection C x := by72 have h := (ProjectionBand.isLUB_inter_Icc_bandProjection C hx).173 ⟨hBC (projection_mem B x), projection_nonneg B hx, projection_le_self B hx⟩74 exact h7576theorem range_projection (B : ProjectionBand E) :77 (projection B).range = B.toBand.toSubmodule := by78 ext x79 constructor80 · rintro ⟨y, rfl⟩81 exact projection_mem B y82 · intro hx83 exact ⟨x, projection_eq_self B hx⟩8485/-- A positive element of the principal band of an atom lies on its ray.86The proof uses norm convergence of its actual truncated principal-ideal net. -/87theorem mem_span_of_mem_atom_band_nonneg [CompleteSpace E]88 (hS : HasSchurProperty ℝ E) {a x : E} (ha : IsLatticeAtom a)89 (hx : 0 ≤ x) (hxa : x ∈ Band.generated ({a} : Set E)) :90 x ∈ Submodule.span ℝ ({a} : Set E) := by91 let y : ℕ → E := fun n => x ⊓ (n : ℝ) • a92 have hy : ∀ n, 0 ≤ y n := fun n =>93 le_inf hx (smul_nonneg (Nat.cast_nonneg _) ha.nonneg)94 have hmono : Monotone y := by95 intro m n hmn96 exact inf_le_inf_left _ (smul_le_smul_of_nonneg_right (Nat.cast_le.mpr hmn) ha.nonneg)97 obtain ⟨z, hz⟩ := SchurLattice.exists_tendsto_of_monotone_norm_bounded hS y hmono ‖x‖98 (fun n => norm_le_norm_of_abs_le_abs (by99 rw [abs_of_nonneg (hy n), abs_of_nonneg hx]100 exact inf_le_left))101 have hlub : IsLUB (Set.range y) x := by102 simpa only [y, Nat.cast_smul_eq_nsmul] using103 (Band.mem_generated_singleton_iff_isLUB_inf_nsmul ha.nonneg hx).mp hxa104 have hzx : z = x := (isLUB_of_tendsto_atTop hmono hz).unique hlub105 have hclosed := (Submodule.span ℝ ({a} : Set E)).closed_of_finiteDimensional106 apply hclosed.mem_of_tendsto (hz.trans (by rw [hzx]))107 exact Filter.Eventually.of_forall (fun n => by108 obtain ⟨t, _, ht⟩ := ha.eq_smul_of_nonneg_le_smul (hy n)109 (Nat.cast_nonneg n) (show y n ≤ (n : ℝ) • a from inf_le_right)110 rw [ht]111 exact Submodule.smul_mem _ t (Submodule.subset_span (Set.mem_singleton a)))112113/-- The principal band of an atom is exactly its one-dimensional real span. -/114theorem atom_band_eq_span [CompleteSpace E] (hS : HasSchurProperty ℝ E)115 {a : E} (ha : IsLatticeAtom a) :116 (Band.generated ({a} : Set E)).toSubmodule = Submodule.span ℝ ({a} : Set E) := by117 apply le_antisymm118 · intro x hx119 have hp := mem_span_of_mem_atom_band_nonneg hS ha (posPart_nonneg x)120 ((Band.generated ({a} : Set E)).toOrderIdeal.posPart_mem hx)121 have hn := mem_span_of_mem_atom_band_nonneg hS ha (negPart_nonneg x)122 ((Band.generated ({a} : Set E)).toOrderIdeal.negPart_mem hx)123 simpa only [posPart_sub_negPart] using (Submodule.span ℝ ({a} : Set E)).sub_mem hp hn124 · apply Submodule.span_le.mpr125 intro x hx126 exact Band.subset_generated _ hx127128/-- Dedekind completeness supplies the projection onto any actual band. -/129def bandOfSchur [CompleteSpace E] (hS : HasSchurProperty ℝ E) (B : Band E) :130 ProjectionBand E :=131 Classical.choose ((ProjectionBand.projectionBand_iff_isLUB_inter_Icc B).mpr (by132 intro x hx133 exact SchurLattice.exists_isLUB hS _134 ⟨0, B.toSubmodule.zero_mem, le_rfl, hx⟩ ⟨x, fun _ hy => hy.2.2⟩))135136theorem bandOfSchur_coe [CompleteSpace E] (hS : HasSchurProperty ℝ E) (B : Band E) :137 (bandOfSchur hS B : Set E) = (B : Set E) :=138 Classical.choose_spec ((ProjectionBand.projectionBand_iff_isLUB_inter_Icc B).mpr (by139 intro x hx140 exact SchurLattice.exists_isLUB hS _141 ⟨0, B.toSubmodule.zero_mem, le_rfl, hx⟩ ⟨x, fun _ hy => hy.2.2⟩))142143def principalBand [CompleteSpace E] (hS : HasSchurProperty ℝ E) (a : E) :144 ProjectionBand E := bandOfSchur hS (Band.generated ({a} : Set E))145146theorem principalBand_coe [CompleteSpace E] (hS : HasSchurProperty ℝ E) (a : E) :147 (principalBand hS a : Set E) = (Band.generated ({a} : Set E) : Set E) :=148 bandOfSchur_coe hS _149150theorem mem_principalBand_self [CompleteSpace E] (hS : HasSchurProperty ℝ E) (a : E) :151 a ∈ principalBand hS a := by152 change a ∈ (principalBand hS a : Set E)153 rw [principalBand_coe]154 exact Band.subset_generated _ (Set.mem_singleton a)155156theorem principalBand_submodule [CompleteSpace E] (hS : HasSchurProperty ℝ E)157 {a : E} (ha : IsLatticeAtom a) :158 (principalBand hS a).toSubmodule = Submodule.span ℝ ({a} : Set E) := by159 have heq : (principalBand hS a).toSubmodule = (Band.generated ({a} : Set E)).toSubmodule :=160 SetLike.coe_injective (principalBand_coe hS a)161 exact heq.trans (atom_band_eq_span hS ha)162163theorem finiteDimensional_principalBand [CompleteSpace E] (hS : HasSchurProperty ℝ E)164 {a : E} (ha : IsLatticeAtom a) : FiniteDimensional ℝ (principalBand hS a).toSubmodule := by165 change @FiniteDimensional ℝ (principalBand hS a).toSubmodule _ _ (Submodule.module _)166 rw [principalBand_submodule hS ha]167 infer_instance168169theorem sup_submodule (B C : ProjectionBand E) :170 (B ⊔ C).toSubmodule = B.toSubmodule ⊔ C.toSubmodule := by171 ext x172 change x ∈ ((B.toBand ⊔ C.toBand : Band E) : Set E) ↔ _173 rw [ProjectionBand.coe_band_sup_eq_add, Submodule.mem_sup]174 constructor175 · rintro ⟨y, hy, z, hz, heq⟩176 exact ⟨y, hy, z, hz, heq.symm⟩177 · rintro ⟨y, hy, z, hz, heq⟩178 exact ⟨y, hy, z, hz, heq.symm⟩179180theorem finiteDimensional_sup (B C : ProjectionBand E)181 [FiniteDimensional ℝ B.toSubmodule] [FiniteDimensional ℝ C.toSubmodule] :182 FiniteDimensional ℝ (B ⊔ C).toSubmodule := by183 change @FiniteDimensional ℝ (B ⊔ C).toSubmodule _ _ (Submodule.module _)184 rw [sup_submodule]185 infer_instance186187/-- Finite suprema retain finite rank. -/188theorem finiteDimensional_finset_sup {ι : Type*} (s : Finset ι) (B : ι → ProjectionBand E)189 (hB : ∀ i ∈ s, FiniteDimensional ℝ (B i).toSubmodule) :190 FiniteDimensional ℝ (s.sup B).toSubmodule := by191 classical192 change @FiniteDimensional ℝ (s.sup B).toSubmodule _ _ (Submodule.module _)193 induction s using Finset.induction_on with194 | empty =>195 change FiniteDimensional ℝ (⊥ : Submodule ℝ E)196 infer_instance197 | @insert a s ha ih =>198 rw [Finset.sup_insert]199 let := hB a (Finset.mem_insert_self a s)200 let := ih (fun i hi => hB i (Finset.mem_insert_of_mem hi))201 exact finiteDimensional_sup _ _202203def cumulative (B : ℕ → ProjectionBand E) (n : ℕ) : ProjectionBand E :=204 (Finset.range (n + 1)).sup B205206theorem cumulative_mono (B : ℕ → ProjectionBand E) : Monotone (cumulative B) := by207 intro m n hmn208 exact Finset.sup_mono (Finset.range_mono (Nat.add_le_add_right hmn 1))209210theorem le_cumulative (B : ℕ → ProjectionBand E) (n : ℕ) : B n ≤ cumulative B n :=211 Finset.le_sup (Finset.mem_range.mpr (Nat.lt_succ_self n))212213/-- Atomicity and eventual coverage by actual bands give strong convergence.214This proves coverage is analytically sufficient, rather than assuming a basis. -/215theorem tendsto_projection_of_atomic_cover [CompleteSpace E]216 (hS : HasSchurProperty ℝ E) (hA : IsAtomicLattice E)217 (B : ℕ → ProjectionBand E) (hmono : Monotone B)218 (hcover : ∀ a : E, IsLatticeAtom a → ∃ n, a ∈ B n) (x : E) :219 Tendsto (fun n => projection (B n) x) atTop (𝓝 x) := by220 have hpos (x : E) (hx : 0 ≤ x) :221 Tendsto (fun n => projection (B n) x) atTop (𝓝 x) := by222 let r : ℕ → E := fun n => x - projection (B n) x223 have hr : ∀ n, 0 ≤ r n := fun n => sub_nonneg.mpr (projection_le_self (B n) hx)224 have hanti : Antitone r := fun m n hmn =>225 sub_le_sub_left (projection_mono (hmono hmn) hx) x226 have hglb : IsGLB (Set.range r) 0 := by227 refine ⟨by rintro _ ⟨n, rfl⟩; exact hr n, ?_⟩228 intro u hu229 by_contra hbad230 have hu0 : u⁺ ≠ 0 := fun heq => hbad (posPart_eq_zero.mp heq)231 obtain ⟨a, ha, hau⟩ := hA u⁺ (lt_of_le_of_ne (posPart_nonneg u) hu0.symm)232 obtain ⟨N, haB⟩ := hcover a ha233 have ha_le : a ≤ r N := hau.trans (sup_le (hu (Set.mem_range_self N)) (hr N))234 have haD : a ∈ disjointComplement (B N : Set E) :=235 (Band.disjointComplement (B N : Set E)).solid236 ((B N).id_sub_bandProjection_mem x) ha.nonneg ha_le237 exact ha.ne_zero (Set.mem_singleton_iff.mp238 (disjointComplement_inter_eq_zero (B N : Set E) ⟨haB, haD⟩))239 have hlim := SchurLattice.tendsto_zero_of_antitone_isGLB hS r hanti hglb240 simpa only [r, sub_sub_cancel, sub_zero] using241 (tendsto_const_nhds (x := x)).sub hlim242 have hp := hpos x⁺ (posPart_nonneg x)243 have hn := hpos x⁻ (negPart_nonneg x)244 simpa only [← map_sub, posPart_sub_negPart] using hp.sub hn245246/-- Increments of increasing band projections are positive operators. -/247theorem positive_difference (B : ℕ → ProjectionBand E) (hmono : Monotone B) (j : ℕ) :248 Positive (UnconditionalDecomposition.difference (fun n => projection (B n)) j).toLinearMap := by249 intro x hx250 cases j with251 | zero => exact projection_nonneg (B 0) hx252 | succ j =>253 exact sub_nonneg.mpr (projection_mono (hmono (Nat.le_succ j)) hx)254255/-- Finite sign transforms of increasing band projections are contractive.256Their positive differences add to a positive contraction dominated by the identity. -/257theorem norm_signed_difference_sum_le (B : ℕ → ProjectionBand E) (hmono : Monotone B)258 (N : ℕ) (ε : ℕ → ℝ) (x : E) (hε : ∀ j, ε j = 1 ∨ ε j = -1) :259 ‖∑ j ∈ Finset.range (N + 1), ε j •260 UnconditionalDecomposition.difference (fun n => projection (B n)) j x‖ ≤ ‖x‖ := by261 let P : ℕ → E →L[ℝ] E := fun n => projection (B n)262 let d := UnconditionalDecomposition.difference P263 have hd (j : ℕ) : |d j x| ≤ d j |x| :=264 Positive.abs_le_map_abs (positive_difference B hmono j) x265 have hb (j : ℕ) : ε j • d j x ≤ d j |x| := by266 rcases hε j with he | he267 · simpa only [he, one_smul] using (le_abs_self (d j x)).trans (hd j)268 · simpa only [he, neg_smul, one_smul] using (neg_le_abs (d j x)).trans (hd j)269 have hbn (j : ℕ) : -(ε j • d j x) ≤ d j |x| := by270 rcases hε j with he | he271 · simpa only [he, one_smul] using (neg_le_abs (d j x)).trans (hd j)272 · simpa only [he, neg_smul, one_smul, neg_neg] using273 (le_abs_self (d j x)).trans (hd j)274 apply norm_le_norm_of_abs_le_abs275 change |∑ j ∈ Finset.range (N + 1), ε j • d j x| ≤ |x|276 apply le_trans (show |∑ j ∈ Finset.range (N + 1), ε j • d j x| ≤277 ∑ j ∈ Finset.range (N + 1), d j |x| from ?_) ?_278 · rw [abs]279 apply sup_le (Finset.sum_le_sum (fun j _ => hb j))280 rw [← Finset.sum_neg_distrib]281 exact Finset.sum_le_sum (fun j _ => hbn j)282 · change (∑ j ∈ Finset.range (N + 1), UnconditionalDecomposition.difference P j |x|) ≤ |x|283 rw [UnconditionalRNP.sum_difference_apply]284 exact projection_le_self (B N) (abs_nonneg x)285286/-- A separable Schur Banach lattice admits an increasing sequence of finite287dimensional bands covering every atom. No atomicity hypothesis is used here. -/288theorem exists_finiteDimensional_band_cover [CompleteSpace E]289 [TopologicalSpace.SeparableSpace E] (hS : HasSchurProperty ℝ E) :290 ∃ B : ℕ → ProjectionBand E, Monotone B ∧291 (∀ n, FiniteDimensional ℝ (B n).toSubmodule) ∧292 ∀ a : E, IsLatticeAtom a → ∃ n, a ∈ B n := by293 classical294 let : Countable (normalizedLatticeAtoms E) := normalizedLatticeAtoms_countable.to_subtype295 let : Encodable (normalizedLatticeAtoms E) := Encodable.ofCountable _296 let C : ℕ → ProjectionBand E := fun n =>297 (Encodable.decode n : Option (normalizedLatticeAtoms E)).elim ⊥ (fun a => principalBand hS a)298 have hopt (o : Option (normalizedLatticeAtoms E)) :299 FiniteDimensional ℝ (o.elim (⊥ : ProjectionBand E) (fun a => principalBand hS a)).toSubmodule := by300 cases o with301 | none =>302 change FiniteDimensional ℝ (⊥ : Submodule ℝ E)303 infer_instance304 | some a => exact finiteDimensional_principalBand hS a.prop.1305 have hC (n : ℕ) : FiniteDimensional ℝ (C n).toSubmodule := hopt _306 refine ⟨cumulative C, cumulative_mono C, fun n =>307 finiteDimensional_finset_sup _ C (fun j _ => hC j), ?_⟩308 intro a ha309 let b : normalizedLatticeAtoms E := ⟨‖a‖⁻¹ • a, ha.normalize, ha.norm_normalize⟩310 let n := Encodable.encode b311 have hn : C n = principalBand hS b := by simp only [C, n, Encodable.encodek, Option.elim_some]312 have hb : (b : E) ∈ cumulative C n :=313 le_cumulative C n (hn.symm ▸ mem_principalBand_self hS b)314 refine ⟨n, ?_⟩315 change a ∈ (cumulative C n).toSubmodule316 have hmem := (cumulative C n).toSubmodule.smul_mem ‖a‖ hb317 simpa only [b, smul_inv_smul₀ (norm_ne_zero_iff.mpr ha.ne_zero)] using hmem318319/-- Full vector-measure RNP for a separable Schur Banach lattice, under the320explicit assertion that every positive nonzero vector dominates an atom. -/321theorem hasRadonNikodymProperty_of_atomic [CompleteSpace E]322 [TopologicalSpace.SeparableSpace E] (hS : HasSchurProperty ℝ E)323 (hA : IsAtomicLattice E) : HasRadonNikodymProperty.{u, v} E := by324 obtain ⟨B, hmono, hfinite, hcover⟩ := exists_finiteDimensional_band_cover hS325 apply UnconditionalRNP.hasRadonNikodymProperty_of_schur_unconditional_projections326 hS (fun n => projection (B n))327 · intro n328 rw [range_projection]329 exact hfinite n330 · intro m n hmn331 exact projection_comp_of_le (hmono hmn)332 · exact tendsto_projection_of_atomic_cover hS hA B hmono hcover333 · exact zero_le_one334 · intro N ε x hε335 simpa only [one_mul] using norm_signed_difference_sum_le B hmono N ε x hε336337end PL1.AtomicBandDecomposition338