PL1/ALFragments.lean
All source files · Download exact source
SHA-256: 348c400c6ab010a2d97242ab5df9a8ec6008794e4f7bd6f454e5337c44b9ff4a
1import PL1.ALOrder2import PL1.LatticeFragments34/-! # Exact fragments in complete AL spaces, without a Schur hypothesis -/56noncomputable section7open Filter Set8open scoped Topology910namespace PL1.ALFragments11open AtomicBandDecomposition SchurLattice LatticeFragments1213variable {E : Type*} [NormedAddCommGroup E] [Lattice E]14 [IsOrderedAddMonoid E] [NormedVectorLattice E]15/-- The principal band of either disjoint piece yields an actual nontrivial16fragment of the original vector. -/17theorem exists_proper_fragment [CompleteSpace E] (hAL : ALRenorming.IsALNorm E)18 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}19 (hu : 0 < u) (hna : ¬ IsLatticeAtom u) :20 ∃ v : E, IsFragment u v ∧ 0 < v ∧ 0 < u - v := by21 obtain ⟨a, b, ha, hau, hb, hbu, hab⟩ := exists_disjoint_nonzero_of_not_atom φ hφ hu hna22 let B := ALOrder.principalBand hAL a23 have hPa : projection B a = a := projection_eq_self B (ALOrder.mem_principalBand_self hAL a)24 have hav : a ≤ projection B u := by25 have h := projection_nonneg B (sub_nonneg.mpr hau)26 rw [map_sub, hPa] at h27 exact sub_nonneg.mp h28 have hbB : b ∈ disjointComplement (B : Set E) := by29 have hgen : (Band.generated ({a} : Set E) : Set E) ⊆ disjointComplement ({b} : Set E) := by30 apply Band.generated_le (B := Band.disjointComplement ({b} : Set E))31 intro x hx32 rcases Set.mem_singleton_iff.mp hx with rfl33 intro y hy34 rcases Set.mem_singleton_iff.mp hy with rfl35 exact hab36 intro y hy37 have hy' : y ∈ (Band.generated ({a} : Set E) : Set E) := by38 change y ∈ (B : Set E) at hy39 simpa only [B, ALOrder.principalBand_coe] using hy40 exact isVLDisjoint_comm.mp (hgen hy' b rfl)41 have hPb : projection B b = 0 := projection_eq_zero B hbB42 have hbrest : b ≤ u - projection B u := by43 have h := projection_le_self B (sub_nonneg.mpr hbu)44 rw [map_sub, hPb, sub_zero] at h45 exact (le_sub_comm).mp h46 exact ⟨projection B u, fragment_projection B hu.le, ha.trans_le hav, hb.trans_le hbrest⟩4748theorem exists_fragment_phi_le_half [CompleteSpace E] (hAL : ALRenorming.IsALNorm E)49 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}50 (hu : 0 < u) (hna : ¬ IsLatticeAtom u) :51 ∃ v : E, IsFragment u v ∧ 0 < v ∧ φ v ≤ φ u / 2 := by52 obtain ⟨v, hv, hvpos, hrpos⟩ := exists_proper_fragment hAL φ hφ hu hna53 by_cases h : φ v ≤ φ u / 254 · exact ⟨v, hv, hvpos, h⟩55 · refine ⟨u - v, hv.compl, hrpos, ?_⟩56 rw [map_sub]57 linarith5859/-- An atomless positive vector has positive fragments of arbitrarily small60strictly-positive-functional mass. -/61theorem exists_small_fragment [CompleteSpace E] (hAL : ALRenorming.IsALNorm E)62 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}63 (hu : 0 < u) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u)64 (δ : ℝ) (hδ : 0 < δ) :65 ∃ v : E, IsFragment u v ∧ 0 < v ∧ φ v < δ := by66 have hseq : ∀ n : ℕ, ∃ v : E, IsFragment u v ∧ 0 < v ∧67 φ v ≤ φ u * (1 / 2 : ℝ) ^ n := by68 intro n69 induction n with70 | zero => exact ⟨u, fragment_self hu.le, hu, by simp⟩71 | succ n ih =>72 obtain ⟨w, hw, hwpos, hφw⟩ := ih73 obtain ⟨v, hv, hvpos, hφv⟩ := exists_fragment_phi_le_half hAL φ hφ hwpos74 (fun ha => hna w ha hw.le)75 refine ⟨v, hw.trans hv, hvpos, ?_⟩76 rw [pow_succ]77 nlinarith78 have ht : Tendsto (fun n : ℕ => φ u * (1 / 2 : ℝ) ^ n) atTop (𝓝 0) := by79 simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2)80 (by norm_num : (1 / 2 : ℝ) < 1)).const_mul (φ u)81 obtain ⟨n, hn⟩ := (ht.eventually_lt_const hδ).exists82 obtain ⟨v, hv, hvpos, hφv⟩ := hseq n83 exact ⟨v, hv, hvpos, hφv.trans_lt hn⟩8485/-- Zorn's lemma and norm convergence of increasing bounded chains produce a86fragment with any prescribed mass in the full scalar interval. -/87theorem exists_fragment_phi_eq [CompleteSpace E] (hAL : ALRenorming.IsALNorm E)88 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}89 (hu : 0 < u) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u)90 (c : ℝ) (hc : 0 ≤ c) (hcu : c ≤ φ u) :91 ∃ v : E, IsFragment u v ∧ φ v = c := by92 classical93 let S : Set E := {v | IsFragment u v ∧ φ v ≤ c}94 have hzero : (0 : E) ∈ S := ⟨fragment_zero hu.le, by simpa using hc⟩95 obtain ⟨v, hv⟩ := zorn_le₀ S (by96 intro C hCS hchain97 rcases C.eq_empty_or_nonempty with rfl | hne98 · exact ⟨0, hzero, by simp⟩99 · let : Nonempty C := ⟨⟨hne.choose, hne.choose_spec⟩⟩100 let : IsDirectedOrder C := ⟨fun a b => by101 rcases hchain.total a.property b.property with hab | hba102 · exact ⟨b, hab, le_rfl⟩103 · exact ⟨a, le_rfl, hba⟩⟩104 have hm : Monotone (Subtype.val : C → E) := fun _ _ h => h105 obtain ⟨z, hz⟩ := ALOrder.exists_tendsto_of_monotone_net_norm_bounded hAL106 (Subtype.val : C → E) hm ‖u‖ (by107 intro w108 have hw := (hCS w.property).1109 apply norm_le_norm_of_abs_le_abs110 simpa only [abs_of_nonneg hw.nonneg, abs_of_nonneg hu.le] using hw.le)111 have hzfrag : IsFragment u z := (isClosed_fragments u).mem_of_tendsto hz112 (Eventually.of_forall (fun w => (hCS w.property).1))113 have hzc : φ z ≤ c := le_of_tendsto' ((φ.continuous.tendsto z).comp hz)114 (fun w => (hCS w.property).2)115 refine ⟨z, ⟨hzfrag, hzc⟩, ?_⟩116 intro w hw117 exact (isLUB_of_tendsto_atTop hm hz).1 ⟨⟨w, hw⟩, rfl⟩)118 have hvfrag : IsFragment u v := hv.1.1119 have hvc : φ v ≤ c := hv.1.2120 refine ⟨v, hvfrag, le_antisymm hvc ?_⟩121 by_contra hcv122 have hgap : 0 < c - φ v := sub_pos.mpr (lt_of_not_ge hcv)123 have hr : 0 < u - v := by124 apply lt_of_le_of_ne (sub_nonneg.mpr hvfrag.le)125 intro hz126 have hφz := congrArg φ hz127 rw [map_zero, map_sub] at hφz128 linarith129 have hnr : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u - v :=130 fun a ha har => hna a ha (har.trans hvfrag.compl.le)131 obtain ⟨w, hw, hwpos, hφw⟩ := exists_small_fragment hAL φ hφ hr hnr _ hgap132 have hsum : v + w ∈ S := by133 refine ⟨hvfrag.add_of_compl hw, ?_⟩134 rw [map_add]135 linarith136 have hmax : v + w ≤ v := hv.2 hsum (le_add_of_nonneg_right hw.nonneg)137 have hwle : w ≤ 0 := by138 have h := sub_nonpos.mpr hmax139 simpa only [add_sub_cancel_left] using h140 exact (not_lt_of_ge hwle) hwpos141142theorem exists_half_fragment [CompleteSpace E] (hAL : ALRenorming.IsALNorm E)143 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}144 (hu : 0 < u) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u) :145 ∃ v : E, 0 ≤ v ∧ v ≤ u ∧ IsVLDisjoint v (u - v) ∧ φ v = φ u / 2 := by146 obtain ⟨v, hv, heq⟩ := exists_fragment_phi_eq hAL φ hφ hu hna (φ u / 2)147 (by linarith [hφ u hu]) (by linarith [hφ u hu])148 exact ⟨v, hv.nonneg, hv.le, hv.disjoint, heq⟩149150end PL1.ALFragments151152