PL1/FiniteDualDisjointization.lean

All source files · Download exact source

SHA-256: 04ee17e38eb2c8d3ceed7f1bb2786b36e163c81c6786121c95c258f67fb48f23

1import PL1.DisjointNormingFunctionals2import BanLat.Substructures.Band.PPP34/-!5Finite dual disjointization. The projection property below is applied to the6conditionally complete strong dual, never assumed for the original lattice.7-/8noncomputable section9open scoped BigOperators10namespace PL1.FiniteDualDisjointization1112variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]13  [VectorLattice X] [HasPrincipalProjectionProperty X]1415lemma exists_selecting_band (x y : X) :16    ∃ P : ProjectionBand X, P.bandProjection (x - y) = (x - y)⁺ := by17  obtain ⟨P, hP⟩ := HasPrincipalProjectionProperty.exists_projectionBand ((x - y)⁺)18  refine ⟨P, ?_⟩19  have hpos : (x-y)⁺ ∈ (P : Set X) := by20    rw [hP]21    exact Band.subset_generated _ rfl22  have hgen : (Band.generated ({(x-y)⁺} : Set X) : Set X) ⊆23      disjointComplement ({(x-y)⁻} : Set X) := by24    apply Band.generated_le (B := Band.disjointComplement ({(x-y)⁻} : Set X))25    rintro z rfl w hw26    rcases Set.mem_singleton_iff.mp hw with rfl27    exact isVLDisjoint_posPart_negPart (x-y)28  have hneg : (x-y)⁻ ∈ disjointComplement (P : Set X) := by29    intro z hz30    have hz' : z ∈ (Band.generated ({(x-y)⁺} : Set X) : Set X) := by31      simpa [hP] using hz32    exact isVLDisjoint_comm.mp (hgen hz' _ (Set.mem_singleton _))33  calc34    P.bandProjection (x-y) = P.bandProjection ((x-y)⁺ - (x-y)⁻) := by35      rw [posPart_sub_negPart]36    _ = (x-y)⁺ := by37      rw [map_sub, P.bandProjection_eq_of_mem hpos,38        P.bandProjection_eq_zero_of_mem_dc hneg, sub_zero]3940/-- Each positive finite family has a disjoint dominated refinement whose sum41majorizes every member of the original family. -/42theorem exists_disjoint_majorizing_refinement (n : ℕ) (ν : Fin n → X)43    (hν : ∀ i, 0 ≤ ν i) :44    ∃ ψ : Fin n → X, (∀ i, 0 ≤ ψ i) ∧ (∀ i, ψ i ≤ ν i) ∧45      (Pairwise fun i j => IsVLDisjoint (ψ i) (ψ j)) ∧46      (∀ i, ν i ≤ ∑ j, ψ j) := by47  classical48  induction n with49  | zero => exact ⟨ν, hν, fun i => le_rfl, fun i => Fin.elim0 i, fun i => Fin.elim0 i⟩50  | succ n ih =>51    obtain ⟨ψ, hψ0, hψle, hψd, hψmaj⟩ := ih (fun i => ν i.succ) (fun i => hν i.succ)52    let q := ∑ i, ψ i53    obtain ⟨P, hP⟩ := exists_selecting_band (ν 0) q54    let w : Fin (n+1) → X := Fin.cons (P.bandProjection (ν 0))55      (fun i => (Pᶜ : ProjectionBand X).bandProjection (ψ i))56    have hproj0 (B : ProjectionBand X) {z : X} (hz : 0 ≤ z) : 0 ≤ B.bandProjection z :=57      Positive.zero_le_iff.mp B.bandProjection_nonneg z hz58    have hprojle (B : ProjectionBand X) {z : X} (hz : 0 ≤ z) : B.bandProjection z ≤ z :=59      Positive.le_iff.mp B.bandProjection_le_id z hz60    have hw0 (i) : 0 ≤ w i := by61      refine Fin.cases ?_ (fun j => ?_) i62      · exact hproj0 P (hν 0)63      · exact hproj0 Pᶜ (hψ0 j)64    have hwle (i) : w i ≤ ν i := by65      refine Fin.cases ?_ (fun j => ?_) i66      · exact hprojle P (hν 0)67      · exact (hprojle Pᶜ (hψ0 j)).trans (hψle j)68    have hwd : Pairwise fun i j => IsVLDisjoint (w i) (w j) := by69      intro i70      refine Fin.cases ?_ (fun a => ?_) i71      · intro j72        refine Fin.cases ?_ (fun b => ?_) j73        all_goals intro hij74        · exact False.elim (hij rfl)75        · exact isVLDisjoint_comm.mp76            ((Pᶜ : ProjectionBand X).bandProjection_mem (ψ b) _ (P.bandProjection_mem (ν 0)))77      · intro j78        refine Fin.cases ?_ (fun b => ?_) j79        all_goals intro hij80        · exact (Pᶜ : ProjectionBand X).bandProjection_mem (ψ a) _ (P.bandProjection_mem (ν 0))81        · have hab : a ≠ b := fun h => hij (congrArg Fin.succ h)82          apply IsVLDisjoint.mono_right83          · apply (hψd hab).mono_left84            rw [abs_of_nonneg (hw0 a.succ), abs_of_nonneg (hψ0 a)]85            exact hprojle Pᶜ (hψ0 a)86          · rw [abs_of_nonneg (hw0 b.succ), abs_of_nonneg (hψ0 b)]87            exact hprojle Pᶜ (hψ0 b)88    have hsum : ∑ i, w i = ν 0 ⊔ q := by89      rw [Fin.sum_univ_succ]90      change P.bandProjection (ν 0) + ∑ i, (Pᶜ : ProjectionBand X).bandProjection (ψ i) = _91      rw [← map_sum, ProjectionBand.bandProjection_compl]92      change P.bandProjection (ν 0) + (q - P.bandProjection q) = _93      have hP' : P.bandProjection (ν 0) - P.bandProjection q = (ν 0-q)⁺ := by94        rw [← map_sub, hP]95      calc96        _ = q + (ν 0-q)⁺ := by rw [← hP']; abel97        _ = ν 0 ⊔ q := (sup_eq_add_posPart_sub _ _).symm98    refine ⟨w, hw0, hwle, hwd, ?_⟩99    intro i100    rw [hsum]101    refine Fin.cases le_sup_left (fun j => ?_) i102    exact (hψmaj j).trans le_sup_right103104end PL1.FiniteDualDisjointization105106107