BanLat/RieszDec.lean
All source files · Download exact source
SHA-256: c6c50461b12c0243b9ebf8efef0a4ad8ffa44e85f0d99148e4257168921da5fa
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Basic67/-!8# The Riesz decomposition theorem910This file collects the Riesz decomposition theorem and its refinements in a lattice-ordered11abelian group: the binary form, the matrix form for two partitions of the same sum, the12version with a finite sum on the left, the absolute-value decomposition, and the13identification of sum intervals.14-/1516open scoped Pointwise1718section LatticeOrderedGroup1920variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]2122/-- Riesz decomposition: if `0 ≤ x ≤ y + z` with `y, z ≥ 0`, then `x = x₁ + x₂`23with `0 ≤ x₁ ≤ y` and `0 ≤ x₂ ≤ z`. -/24theorem riesz_decomposition (x y z : X) (xnonneg : 0 ≤ x) (ynonneg : 0 ≤ y)25 (znonneg : 0 ≤ z) (h : x ≤ y + z) : ∃ x1 x2 : X, (0 ≤ x1) ∧ (x1 ≤ y) ∧26 (0 ≤ x2) ∧ (x2 ≤ z) ∧ (x = x1 + x2) := by27 use (x ⊓ y); use (x - x ⊓ y)28 repeat (any_goals constructor)29 · exact le_inf xnonneg ynonneg30 · exact inf_le_right31 · simp32 · rw [sub_inf]33 have : x - y ≤ z := by34 calc35 x - y = x + (-y) := by rw [sub_eq_add_neg]36 _ ≤ (y + z) + (-y) := by apply add_le_add h (le_refl (-y))37 _ ≤ z := by simp38 rw [le_iff_posPart_negPart] at this39 rw [sub_self, sup_comm, ← posPart_def]40 rw [← posPart_of_nonneg znonneg]41 exact this.142 · simp4344private lemma riesz_split_sum :45 ∀ {n : ℕ} (u : X) (z : Fin n → X), 0 ≤ u → (∀ j, 0 ≤ z j) →46 u ≤ ∑ j, z j →47 ∃ x : Fin n → X, (∀ j, 0 ≤ x j) ∧ (∀ j, x j ≤ z j) ∧ u = ∑ j, x j := by48 intro n49 induction n with50 | zero =>51 intro u z hu _ h52 refine ⟨Fin.elim0, fun j => j.elim0, fun j => j.elim0, ?_⟩53 rw [Fin.sum_univ_zero] at h ⊢54 exact le_antisymm h hu55 | succ n ih =>56 intro u z hu hz h57 rw [Fin.sum_univ_succ] at h58 obtain ⟨a, b, ha_nn, ha_le, hb_nn, hb_le, hab⟩ :=59 riesz_decomposition u (z 0) (∑ j : Fin n, z j.succ) hu (hz 0)60 (Finset.sum_nonneg fun j _ => hz _) h61 obtain ⟨x', hx'_nn, hx'_le, hx'_sum⟩ :=62 ih b (fun j => z j.succ) hb_nn (fun j => hz _) hb_le63 refine ⟨Fin.cons a x', ?_, ?_, ?_⟩64 · intro j65 induction j using Fin.cases with66 | zero => simpa using ha_nn67 | succ i => simpa using hx'_nn i68 · intro j69 induction j using Fin.cases with70 | zero => simpa using ha_le71 | succ i => simpa using hx'_le i72 · rw [Fin.sum_univ_succ, Fin.cons_zero]73 simp only [Fin.cons_succ]74 rw [hab, hx'_sum]7576/-- Matrix form of Riesz decomposition: if two finite sums of non-negative vectors agree,77there is a non-negative matrix whose row sums recover the first family and whose column78sums recover the second. -/79theorem riesz_decomposition_matrix :80 ∀ {m n : ℕ} (u : Fin m → X) (z : Fin n → X),81 (∀ i, 0 ≤ u i) → (∀ j, 0 ≤ z j) → ∑ i, u i = ∑ j, z j →82 ∃ x : Fin m → Fin n → X,83 (∀ i j, 0 ≤ x i j) ∧84 (∀ i, u i = ∑ j, x i j) ∧85 (∀ j, z j = ∑ i, x i j) := by86 intro m87 induction m with88 | zero =>89 intro n u z _ hz heq90 refine ⟨fun i _ => i.elim0, fun i => i.elim0, fun i => i.elim0, ?_⟩91 intro j92 have h0 : ∑ j, z j = 0 := by rw [← heq, Fin.sum_univ_zero]93 have hzj : z j ≤ 0 := by94 have := Finset.single_le_sum (f := z) (fun j' _ => hz j') (Finset.mem_univ j)95 rw [h0] at this; exact this96 rw [le_antisymm hzj (hz j)]97 exact (Fin.sum_univ_zero _).symm98 | succ m ih =>99 intro n u z hu hz heq100 have hu0_le : u 0 ≤ ∑ j, z j := by101 rw [← heq, Fin.sum_univ_succ]102 exact le_add_of_nonneg_right (Finset.sum_nonneg fun i _ => hu _)103 obtain ⟨x0, hx0_nn, hx0_le, hx0_sum⟩ :=104 riesz_split_sum (u 0) z (hu 0) hz hu0_le105 let z' : Fin n → X := fun j => z j - x0 j106 have hz'_nn : ∀ j, 0 ≤ z' j := fun j => sub_nonneg.mpr (hx0_le j)107 have heq' : ∑ i, (u ∘ Fin.succ) i = ∑ j, z' j := by108 rw [Fin.sum_univ_succ] at heq109 have hsum_sub : ∑ j, z' j = (∑ j, z j) - ∑ j, x0 j := by110 simp [z', Finset.sum_sub_distrib]111 rw [hsum_sub, ← heq, ← hx0_sum]112 simp [Function.comp]113 obtain ⟨y, hy_nn, hy_row, hy_col⟩ :=114 ih (u ∘ Fin.succ) z' (fun i => hu _) hz'_nn heq'115 refine ⟨Fin.cons x0 y, ?_, ?_, ?_⟩116 · intro i j117 induction i using Fin.cases with118 | zero => simpa using hx0_nn j119 | succ i => simpa using hy_nn i j120 · intro i121 induction i using Fin.cases with122 | zero =>123 simp only [Fin.cons_zero]124 rw [hx0_sum]125 | succ i =>126 simp only [Fin.cons_succ]127 exact hy_row i128 · intro j129 rw [Fin.sum_univ_succ, Fin.cons_zero]130 simp only [Fin.cons_succ]131 have hz'_eq : z j - x0 j = ∑ i, y i j := hy_col j132 have : z j = x0 j + (z j - x0 j) := by abel133 rw [this, hz'_eq]134135/-- Riesz decomposition with several summands on the left: if `∑ᵢ uᵢ ≤ x + y` with all136terms non-negative, each `uᵢ` splits as `vᵢ + wᵢ` so that `∑ᵢ vᵢ ≤ x` and `∑ᵢ wᵢ ≤ y`. -/137theorem riesz_decomposition_sum_le {k : ℕ} (u : Fin k → X) (x y : X)138 (hu : ∀ i, 0 ≤ u i) (hx : 0 ≤ x) (hy : 0 ≤ y)139 (h : ∑ i, u i ≤ x + y) :140 ∃ v w : Fin k → X,141 (∀ i, 0 ≤ v i) ∧ (∀ i, 0 ≤ w i) ∧142 (∑ i, v i ≤ x) ∧ (∑ i, w i ≤ y) ∧143 (∀ i, u i = v i + w i) := by144 obtain ⟨a, b, ha_nn, ha_le, hb_nn, hb_le, hab⟩ :=145 riesz_decomposition (∑ i, u i) x y (Finset.sum_nonneg fun i _ => hu _) hx hy h146 let z : Fin 2 → X := ![a, b]147 have hz_nn : ∀ j, 0 ≤ z j := by148 intro j; fin_cases j149 · exact ha_nn150 · exact hb_nn151 have hsum_eq : ∑ i, u i = ∑ j, z j := by152 rw [hab, Fin.sum_univ_two]153 rfl154 obtain ⟨M, hM_nn, hM_row, hM_col⟩ :=155 riesz_decomposition_matrix u z hu hz_nn hsum_eq156 refine ⟨fun i => M i 0, fun i => M i 1, ?_, ?_, ?_, ?_, ?_⟩157 · intro i; exact hM_nn i 0158 · intro i; exact hM_nn i 1159 · have hcol := hM_col 0160 have : a = ∑ i, M i 0 := hcol161 rw [← this]; exact ha_le162 · have hcol := hM_col 1163 have : b = ∑ i, M i 1 := hcol164 rw [← this]; exact hb_le165 · intro i166 have := hM_row i167 rw [Fin.sum_univ_two] at this168 exact this169170/-- Decomposing a vector according to a splitting of its absolute value: if `|x| = u + v`171with `u, v ≥ 0`, then `x = y + z` for some `y, z` with `|y| = u` and `|z| = v`. -/172theorem exists_abs_decomposition {x u v : X} (hu : 0 ≤ u) (hv : 0 ≤ v)173 (h : |x| = u + v) :174 ∃ y z : X, x = y + z ∧ |y| = u ∧ |z| = v := by175 set a := x⁺ ⊓ u with ha_def176 set b := x⁻ ⊓ u with hb_def177 have ha_nn : 0 ≤ a := le_inf (posPart_nonneg _) hu178 have hb_nn : 0 ≤ b := le_inf (negPart_nonneg _) hu179 have ha_le_pp : a ≤ x⁺ := inf_le_left180 have hb_le_np : b ≤ x⁻ := inf_le_left181 have ha_le_u : a ≤ u := inf_le_right182 have hb_le_u : b ≤ u := inf_le_right183 have hab_disj : a ⊓ b = 0 := by184 apply le_antisymm _ (le_inf ha_nn hb_nn)185 calc a ⊓ b ≤ x⁺ ⊓ x⁻ := inf_le_inf ha_le_pp hb_le_np186 _ = 0 := posPart_inf_negPart_eq_zero _187 have hab_eq : a + b = u := by188 have hle : a + b ≤ u := by189 have e : a + b = a ⊔ b := by190 have := inf_add_sup a b191 rw [hab_disj, zero_add] at this192 exact this.symm193 rw [e]; exact sup_le ha_le_u hb_le_u194 have hge : u ≤ a + b := by195 have hle_u : u ≤ x⁺ + x⁻ := by196 rw [posPart_add_negPart, h]197 exact le_add_of_nonneg_right hv198 obtain ⟨u₁, u₂, h1_nn, h1_le, h2_nn, h2_le, huuv⟩ :=199 riesz_decomposition u x⁺ x⁻ hu (posPart_nonneg _) (negPart_nonneg _) hle_u200 have h1a : u₁ ≤ a := le_inf h1_le (by rw [huuv]; exact le_add_of_nonneg_right h2_nn)201 have h2b : u₂ ≤ b := le_inf h2_le (by rw [huuv]; exact le_add_of_nonneg_left h1_nn)202 rw [huuv]; exact add_le_add h1a h2b203 exact le_antisymm hle hge204 let y := a - b205 refine ⟨y, x - y, by abel, ?_, ?_⟩206 · have hy_pp : y⁺ = a := (uniqueness_posPart y rfl hab_disj).symm207 have hy_np : y⁻ = b := by208 have hneg : -y = b - a := by simp [y]209 have hba_disj : b ⊓ a = 0 := by rw [inf_comm]; exact hab_disj210 have h1 : (-y)⁺ = b := (uniqueness_posPart (-y) hneg hba_disj).symm211 rw [← posPart_neg]; exact h1212 rw [← posPart_add_negPart, hy_pp, hy_np, hab_eq]213 · -- |x - y| = v214 -- z = x - y = (x⁺ - a) - (x⁻ - b)215 set a' := x⁺ - a with ha'_def216 set b' := x⁻ - b with hb'_def217 have ha'_nn : 0 ≤ a' := sub_nonneg.mpr ha_le_pp218 have hb'_nn : 0 ≤ b' := sub_nonneg.mpr hb_le_np219 have ha'_le_pp : a' ≤ x⁺ := sub_le_self _ ha_nn220 have hb'_le_np : b' ≤ x⁻ := sub_le_self _ hb_nn221 have hab'_disj : a' ⊓ b' = 0 := by222 apply le_antisymm _ (le_inf ha'_nn hb'_nn)223 calc a' ⊓ b' ≤ x⁺ ⊓ x⁻ := inf_le_inf ha'_le_pp hb'_le_np224 _ = 0 := posPart_inf_negPart_eq_zero _225 have hxy : x - y = a' - b' := by226 change x - (a - b) = (x⁺ - a) - (x⁻ - b)227 conv_lhs => rw [← posPart_sub_negPart x]228 abel229 have hz_pp : (x - y)⁺ = a' := by230 rw [hxy]; exact (uniqueness_posPart _ rfl hab'_disj).symm231 have hz_np : (x - y)⁻ = b' := by232 rw [hxy]233 have hneg : -(a' - b') = b' - a' := by abel234 have hba'_disj : b' ⊓ a' = 0 := by rw [inf_comm]; exact hab'_disj235 have h1 : (-(a' - b'))⁺ = b' := (uniqueness_posPart _ hneg hba'_disj).symm236 rw [← posPart_neg]; exact h1237 have hab'_sum : a' + b' = v := by238 have key : (a + b) + (a' + b') = u + v := by239 change (a + b) + ((x⁺ - a) + (x⁻ - b)) = u + v240 rw [← h, ← posPart_add_negPart]241 abel242 rw [hab_eq] at key243 exact add_left_cancel key244 rw [← posPart_add_negPart, hz_pp, hz_np, hab'_sum]245246/-- Riesz decomposition for the absolute value: if `|x| ≤ v₁ + ⋯ + vₙ` with each `vᵢ ≥ 0`,247then `x = x₁ + ⋯ + xₙ` with `|xᵢ| ≤ |x| ⊓ vᵢ`. -/248theorem riesz_decomposition_abs :249 ∀ {n : ℕ} (x : X) (v : Fin n → X),250 (∀ i, 0 ≤ v i) → |x| ≤ ∑ i, v i →251 ∃ y : Fin n → X, x = ∑ i, y i ∧ ∀ i, |y i| ≤ |x| ⊓ v i := by252 intro n253 induction n with254 | zero =>255 intro x v _ h256 rw [Fin.sum_univ_zero] at h257 have habs : |x| = 0 := le_antisymm h (abs_nonneg _)258 have hx : x = 0 := (abs_eq_zero_iff_zero x).mp habs259 refine ⟨Fin.elim0, ?_, ?_⟩260 · rw [Fin.sum_univ_zero]; exact hx261 · intro i; exact i.elim0262 | succ n ih =>263 intro x v hv h264 rw [Fin.sum_univ_succ] at h265 -- Split |x| = u + w with 0 ≤ u ≤ v 0 and 0 ≤ w ≤ ∑ v i.succ266 obtain ⟨u, w, hu_nn, hu_le, hw_nn, hw_le, huw⟩ :=267 riesz_decomposition |x| (v 0) (∑ i : Fin n, v i.succ) (abs_nonneg _) (hv 0)268 (Finset.sum_nonneg fun i _ => hv _) h269 -- Split x = y0 + x' with |y0| = u and |x'| = w270 obtain ⟨y0, x', hxsum, hy0_abs, hx'_abs⟩ := exists_abs_decomposition hu_nn hw_nn huw271 -- Apply ih to x' and v ∘ Fin.succ272 have hx'_le : |x'| ≤ ∑ i : Fin n, v i.succ := hx'_abs ▸ hw_le273 obtain ⟨y', hy'_sum, hy'_abs⟩ := ih x' (fun i => v i.succ) (fun i => hv _) hx'_le274 refine ⟨Fin.cons y0 y', ?_, ?_⟩275 · rw [Fin.sum_univ_succ, Fin.cons_zero]276 simp only [Fin.cons_succ]277 rw [hxsum, hy'_sum]278 · intro i279 induction i using Fin.cases with280 | zero =>281 simp only [Fin.cons_zero]282 refine le_inf ?_ ?_283 · rw [hy0_abs, huw]; exact le_add_of_nonneg_right hw_nn284 · rw [hy0_abs]; exact hu_le285 | succ i =>286 simp only [Fin.cons_succ]287 have h1 : |y' i| ≤ |x'| ⊓ v i.succ := hy'_abs i288 have h2 : |x'| ≤ |x| := by289 rw [hx'_abs, huw]290 exact le_add_of_nonneg_left hu_nn291 exact h1.trans (inf_le_inf_right _ h2)292293/-- The order intervals of non-negative endpoints satisfy `[0, x] + [0, y] = [0, x + y]`. -/294theorem Icc_add_Icc_of_nonneg {x y : X} (hx : 0 ≤ x) (hy : 0 ≤ y) :295 Set.Icc (0 : X) x + Set.Icc (0 : X) y = Set.Icc (0 : X) (x + y) := by296 ext c297 rw [Set.mem_add]298 constructor299 · rintro ⟨a, ha, b, hb, rfl⟩300 exact ⟨add_nonneg ha.1 hb.1, add_le_add ha.2 hb.2⟩301 · rintro ⟨hc0, hc⟩302 obtain ⟨a, b, ha0, ha, hb0, hb, heq⟩ := riesz_decomposition c x y hc0 hx hy hc303 exact ⟨a, ⟨ha0, ha⟩, b, ⟨hb0, hb⟩, heq.symm⟩304305end LatticeOrderedGroup306