PL1/LatticeFragments.lean
All source files · Download exact source
SHA-256: b3effd7e26196233052be5fc3135266d1cd6e06c94acf7d7ef7294284bbe4753
1import PL1.AtomicBandDecomposition2import PL1.LatticeStrictPositive3import Mathlib.Order.Zorn45/-! # Genuine disjoint fragments of positive lattice vectors -/67noncomputable section8open Filter Set9open scoped Topology1011namespace PL1.LatticeFragments12open AtomicBandDecomposition SchurLattice1314variable {E : Type*} [NormedAddCommGroup E] [Lattice E]15 [IsOrderedAddMonoid E] [NormedVectorLattice E]1617/-- A positive fragment of u, with disjoint positive remainder. -/18def IsFragment (u v : E) : Prop := 0 ≤ v ∧ v ≤ u ∧ IsVLDisjoint v (u - v)1920omit [IsOrderedAddMonoid E] [NormedVectorLattice E] in21theorem IsFragment.nonneg {u v : E} (h : IsFragment u v) : 0 ≤ v := h.122omit [IsOrderedAddMonoid E] [NormedVectorLattice E] in23theorem IsFragment.le {u v : E} (h : IsFragment u v) : v ≤ u := h.2.124omit [IsOrderedAddMonoid E] [NormedVectorLattice E] in25theorem IsFragment.disjoint {u v : E} (h : IsFragment u v) : IsVLDisjoint v (u - v) := h.2.22627omit [NormedVectorLattice E] in28theorem fragment_zero {u : E} (hu : 0 ≤ u) : IsFragment u 0 :=29 ⟨le_rfl, hu, isVLDisjoint_zero_left _⟩3031omit [NormedVectorLattice E] in32theorem fragment_self {u : E} (hu : 0 ≤ u) : IsFragment u u :=33 ⟨hu, le_rfl, by simpa using isVLDisjoint_zero_right u⟩3435omit [NormedVectorLattice E] in36theorem IsFragment.compl {u v : E} (h : IsFragment u v) : IsFragment u (u - v) := by37 refine ⟨sub_nonneg.mpr h.le, sub_le_self _ h.nonneg, ?_⟩38 simpa only [sub_sub_cancel] using isVLDisjoint_comm.mp h.disjoint3940omit [NormedVectorLattice E] in41theorem IsFragment.trans {u v w : E} (hv : IsFragment u v) (hw : IsFragment v w) :42 IsFragment u w := by43 refine ⟨hw.nonneg, hw.le.trans hv.le, ?_⟩44 have hd : IsVLDisjoint w (u - v) := hv.disjoint.mono_left (by45 simpa only [abs_of_nonneg hw.nonneg, abs_of_nonneg hv.nonneg] using hw.le)46 have he : u - w = (u - v) + (v - w) := by abel47 rw [he]48 exact hd.add_right hw.disjoint4950omit [NormedVectorLattice E] in51theorem IsFragment.add_of_compl {u v w : E} (hv : IsFragment u v)52 (hw : IsFragment (u - v) w) : IsFragment u (v + w) := by53 have hvw : v + w ≤ u := by54 have hh : w + v ≤ u := le_sub_iff_add_le.mp hw.le55 simpa only [add_comm] using hh56 refine ⟨add_nonneg hv.nonneg hw.nonneg, hvw, ?_⟩57 have he : u - (v + w) = (u - v) - w := by abel58 rw [he]59 exact (hv.disjoint.mono_right (by60 rw [abs_of_nonneg (sub_nonneg.mpr hw.le), abs_of_nonneg (sub_nonneg.mpr hv.le)]61 exact sub_le_self _ hw.nonneg)).add_left hw.disjoint6263theorem isClosed_fragments (u : E) : IsClosed {v | IsFragment u v} := by64 have hab : Continuous (|·| : E → E) := NormedVectorLattice.lipschitzWith_abs.continuous65 have hc : Continuous (fun v : E => |v| ⊓ |u - v|) :=66 hab.inf (hab.comp (continuous_const.sub continuous_id))67 exact isClosed_Ici.inter (isClosed_Iic.inter (isClosed_eq hc continuous_const))6869theorem fragment_projection (B : ProjectionBand E) {u : E} (hu : 0 ≤ u) :70 IsFragment u (projection B u) := by71 refine ⟨projection_nonneg B hu, projection_le_self B hu, ?_⟩72 exact isVLDisjoint_comm.mp (B.id_sub_bandProjection_mem u _ (projection_mem B u))7374theorem phi_mono (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {x y : E} (hxy : x ≤ y) :75 φ x ≤ φ y := by76 have hp := StrongDual.apply_nonneg_of_nonneg hφ.nonneg (sub_nonneg.mpr hxy)77 rw [map_sub] at hp78 exact sub_nonneg.mp hp7980/-- A nonatom has two disjoint nonzero positive vectors below it. A strictly81positive functional chooses the scalar separating their positive parts. -/82theorem exists_disjoint_nonzero_of_not_atom (φ : E →L[ℝ] ℝ)83 (hφ : IsStrictlyPositive φ) {u : E} (hu : 0 < u) (hna : ¬ IsLatticeAtom u) :84 ∃ a b : E, 0 < a ∧ a ≤ u ∧ 0 < b ∧ b ≤ u ∧ IsVLDisjoint a b := by85 classical86 have hbad : ¬ ∀ x : E, 0 ≤ x → x ≤ u → ∃ t : ℝ, 0 ≤ t ∧ x = t • u :=87 fun h => hna ⟨hu, h⟩88 push Not at hbad89 obtain ⟨x, hx, hxu, hbad⟩ := hbad90 let t : ℝ := φ x / φ u91 have hφu : 0 < φ u := hφ u hu92 have ht : 0 ≤ t := div_nonneg (StrongDual.apply_nonneg_of_nonneg hφ.nonneg hx) hφu.le93 have ht1 : t ≤ 1 := (div_le_one hφu).mpr (phi_mono φ hφ hxu)94 let z : E := x - t • u95 have hz : z ≠ 0 := by96 intro he97 exact hbad t ht (sub_eq_zero.mp he)98 have hφz : φ z = 0 := by99 simp only [z, t, map_sub, map_smul, smul_eq_mul]100 field_simp [hφu.ne']101 ring102 have he : φ z⁺ = φ z⁻ := by103 have h := congrArg φ (posPart_sub_negPart z)104 rw [map_sub, hφz] at h105 exact sub_eq_zero.mp h106 have hp : z⁺ ≠ 0 := by107 intro h108 have hφn : φ z⁻ = 0 := by rw [← he, h, map_zero]109 have hn := hφ.eq_zero_of_nonneg (negPart_nonneg z) hφn110 exact hz (by rw [← posPart_sub_negPart z, h, hn, sub_self])111 have hn : z⁻ ≠ 0 := by112 intro h113 have hφp : φ z⁺ = 0 := by rw [he, h, map_zero]114 exact hp (hφ.eq_zero_of_nonneg (posPart_nonneg z) hφp)115 have htu : t • u ≤ u := by simpa only [one_smul] using116 smul_le_smul_of_nonneg_right ht1 hu.le117 have hpbound : z⁺ ≤ u := sup_le ((sub_le_self _ (smul_nonneg ht hu.le)).trans hxu) hu.le118 have hnbound : z⁻ ≤ u := sup_le (by119 change -(x - t • u) ≤ u120 rw [neg_sub]121 exact (sub_le_self _ hx).trans htu) hu.le122 exact ⟨z⁺, z⁻, lt_of_le_of_ne (posPart_nonneg z) hp.symm, hpbound,123 lt_of_le_of_ne (negPart_nonneg z) hn.symm, hnbound,124 isVLDisjoint_of_inf_eq_zero (posPart_inf_negPart_eq_zero z)⟩125126/-- The principal band of either disjoint piece yields an actual nontrivial127fragment of the original vector. -/128theorem exists_proper_fragment [CompleteSpace E] (hS : HasSchurProperty ℝ E)129 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}130 (hu : 0 < u) (hna : ¬ IsLatticeAtom u) :131 ∃ v : E, IsFragment u v ∧ 0 < v ∧ 0 < u - v := by132 obtain ⟨a, b, ha, hau, hb, hbu, hab⟩ := exists_disjoint_nonzero_of_not_atom φ hφ hu hna133 let B := principalBand hS a134 have hPa : projection B a = a := projection_eq_self B (mem_principalBand_self hS a)135 have hav : a ≤ projection B u := by136 have h := projection_nonneg B (sub_nonneg.mpr hau)137 rw [map_sub, hPa] at h138 exact sub_nonneg.mp h139 have hbB : b ∈ disjointComplement (B : Set E) := by140 have hgen : (Band.generated ({a} : Set E) : Set E) ⊆ disjointComplement ({b} : Set E) := by141 apply Band.generated_le (B := Band.disjointComplement ({b} : Set E))142 intro x hx143 rcases Set.mem_singleton_iff.mp hx with rfl144 intro y hy145 rcases Set.mem_singleton_iff.mp hy with rfl146 exact hab147 intro y hy148 have hy' : y ∈ (Band.generated ({a} : Set E) : Set E) := by149 change y ∈ (B : Set E) at hy150 simpa only [B, principalBand_coe] using hy151 exact isVLDisjoint_comm.mp (hgen hy' b rfl)152 have hPb : projection B b = 0 := projection_eq_zero B hbB153 have hbrest : b ≤ u - projection B u := by154 have h := projection_le_self B (sub_nonneg.mpr hbu)155 rw [map_sub, hPb, sub_zero] at h156 exact (le_sub_comm).mp h157 exact ⟨projection B u, fragment_projection B hu.le, ha.trans_le hav, hb.trans_le hbrest⟩158159theorem exists_fragment_phi_le_half [CompleteSpace E] (hS : HasSchurProperty ℝ E)160 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}161 (hu : 0 < u) (hna : ¬ IsLatticeAtom u) :162 ∃ v : E, IsFragment u v ∧ 0 < v ∧ φ v ≤ φ u / 2 := by163 obtain ⟨v, hv, hvpos, hrpos⟩ := exists_proper_fragment hS φ hφ hu hna164 by_cases h : φ v ≤ φ u / 2165 · exact ⟨v, hv, hvpos, h⟩166 · refine ⟨u - v, hv.compl, hrpos, ?_⟩167 rw [map_sub]168 linarith169170/-- An atomless positive vector has positive fragments of arbitrarily small171strictly-positive-functional mass. -/172theorem exists_small_fragment [CompleteSpace E] (hS : HasSchurProperty ℝ E)173 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}174 (hu : 0 < u) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u)175 (δ : ℝ) (hδ : 0 < δ) :176 ∃ v : E, IsFragment u v ∧ 0 < v ∧ φ v < δ := by177 have hseq : ∀ n : ℕ, ∃ v : E, IsFragment u v ∧ 0 < v ∧178 φ v ≤ φ u * (1 / 2 : ℝ) ^ n := by179 intro n180 induction n with181 | zero => exact ⟨u, fragment_self hu.le, hu, by simp⟩182 | succ n ih =>183 obtain ⟨w, hw, hwpos, hφw⟩ := ih184 obtain ⟨v, hv, hvpos, hφv⟩ := exists_fragment_phi_le_half hS φ hφ hwpos185 (fun ha => hna w ha hw.le)186 refine ⟨v, hw.trans hv, hvpos, ?_⟩187 rw [pow_succ]188 nlinarith189 have ht : Tendsto (fun n : ℕ => φ u * (1 / 2 : ℝ) ^ n) atTop (𝓝 0) := by190 simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2)191 (by norm_num : (1 / 2 : ℝ) < 1)).const_mul (φ u)192 obtain ⟨n, hn⟩ := (ht.eventually_lt_const hδ).exists193 obtain ⟨v, hv, hvpos, hφv⟩ := hseq n194 exact ⟨v, hv, hvpos, hφv.trans_lt hn⟩195196/-- Zorn's lemma and norm convergence of increasing bounded chains produce a197fragment with any prescribed mass in the full scalar interval. -/198theorem exists_fragment_phi_eq [CompleteSpace E] (hS : HasSchurProperty ℝ E)199 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}200 (hu : 0 < u) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u)201 (c : ℝ) (hc : 0 ≤ c) (hcu : c ≤ φ u) :202 ∃ v : E, IsFragment u v ∧ φ v = c := by203 classical204 let S : Set E := {v | IsFragment u v ∧ φ v ≤ c}205 have hzero : (0 : E) ∈ S := ⟨fragment_zero hu.le, by simpa using hc⟩206 obtain ⟨v, hv⟩ := zorn_le₀ S (by207 intro C hCS hchain208 rcases C.eq_empty_or_nonempty with rfl | hne209 · exact ⟨0, hzero, by simp⟩210 · let : Nonempty C := ⟨⟨hne.choose, hne.choose_spec⟩⟩211 let : IsDirectedOrder C := ⟨fun a b => by212 rcases hchain.total a.property b.property with hab | hba213 · exact ⟨b, hab, le_rfl⟩214 · exact ⟨a, le_rfl, hba⟩⟩215 have hm : Monotone (Subtype.val : C → E) := fun _ _ h => h216 obtain ⟨z, hz⟩ := exists_tendsto_of_monotone_net_norm_bounded hS217 (Subtype.val : C → E) hm ‖u‖ (by218 intro w219 have hw := (hCS w.property).1220 apply norm_le_norm_of_abs_le_abs221 simpa only [abs_of_nonneg hw.nonneg, abs_of_nonneg hu.le] using hw.le)222 have hzfrag : IsFragment u z := (isClosed_fragments u).mem_of_tendsto hz223 (Eventually.of_forall (fun w => (hCS w.property).1))224 have hzc : φ z ≤ c := le_of_tendsto' ((φ.continuous.tendsto z).comp hz)225 (fun w => (hCS w.property).2)226 refine ⟨z, ⟨hzfrag, hzc⟩, ?_⟩227 intro w hw228 exact (isLUB_of_tendsto_atTop hm hz).1 ⟨⟨w, hw⟩, rfl⟩)229 have hvfrag : IsFragment u v := hv.1.1230 have hvc : φ v ≤ c := hv.1.2231 refine ⟨v, hvfrag, le_antisymm hvc ?_⟩232 by_contra hcv233 have hgap : 0 < c - φ v := sub_pos.mpr (lt_of_not_ge hcv)234 have hr : 0 < u - v := by235 apply lt_of_le_of_ne (sub_nonneg.mpr hvfrag.le)236 intro hz237 have hφz := congrArg φ hz238 rw [map_zero, map_sub] at hφz239 linarith240 have hnr : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u - v :=241 fun a ha har => hna a ha (har.trans hvfrag.compl.le)242 obtain ⟨w, hw, hwpos, hφw⟩ := exists_small_fragment hS φ hφ hr hnr _ hgap243 have hsum : v + w ∈ S := by244 refine ⟨hvfrag.add_of_compl hw, ?_⟩245 rw [map_add]246 linarith247 have hmax : v + w ≤ v := hv.2 hsum (le_add_of_nonneg_right hw.nonneg)248 have hwle : w ≤ 0 := by249 have h := sub_nonpos.mpr hmax250 simpa only [add_sub_cancel_left] using h251 exact (not_lt_of_ge hwle) hwpos252253theorem exists_half_fragment [CompleteSpace E] (hS : HasSchurProperty ℝ E)254 (φ : E →L[ℝ] ℝ) (hφ : IsStrictlyPositive φ) {u : E}255 (hu : 0 < u) (hna : ∀ a : E, IsLatticeAtom a → ¬ a ≤ u) :256 ∃ v : E, 0 ≤ v ∧ v ≤ u ∧ IsVLDisjoint v (u - v) ∧ φ v = φ u / 2 := by257 obtain ⟨v, hv, heq⟩ := exists_fragment_phi_eq hS φ hφ hu hna (φ u / 2)258 (by linarith [hφ u hu]) (by linarith [hφ u hu])259 exact ⟨v, hv.nonneg, hv.le, hv.disjoint, heq⟩260261end PL1.LatticeFragments262