PL1/PositiveLowerOneBridge.lean
All source files · Download exact source
SHA-256: 9ea8851b685ef03d86d6e59ebac0c9086ca4e33bd829f9cf21604443413fb4a0
1import PL1.FiniteDualDisjointization2import PL1.ALRenorming34/-!5# From disjoint to positive lower-one estimates67All primal disjointizations are finite approximations from Riesz–Kantorovich.8Only the dual uses principal bands, supplied by its existing order completeness.9-/10noncomputable section11open scoped BigOperators12namespace PL1.PositiveLowerOneBridge1314variable {E : Type*} [NormedAddCommGroup E] [Lattice E]15 [IsOrderedAddMonoid E] [BanachLattice E]1617lemma dual_sup_approx (φ ψ : StrongDual ℝ E) {u : E} (hu : 0 ≤ u)18 {ε : ℝ} (hε : 0 < ε) :19 ∃ y z : E, 0 ≤ y ∧ 0 ≤ z ∧ y+z=u ∧ (φ ⊔ ψ) u - ε < φ y + ψ z := by20 have hL : IsLUB21 {r : ℝ | ∃ y z : E, 0 ≤ y ∧ 0 ≤ z ∧ y+z=u ∧ r=φ y+ψ z}22 ((φ ⊔ ψ) u) := OrderDualSpace.isLUB_sup_apply (φ := φ.toOrderDualSpace)23 (ψ := ψ.toOrderDualSpace) hu24 by_contra! h25 have hle : (φ ⊔ ψ) u ≤ (φ ⊔ ψ) u - ε := hL.2 (by26 rintro r ⟨y,z,hy,hz,hyz,rfl⟩27 exact h y z hy hz hyz)28 linarith2930lemma disjoint_dual_sum (n : ℕ) (φ : StrongDual ℝ E) (ψ : Fin n → StrongDual ℝ E)31 (h : ∀ i, IsVLDisjoint φ (ψ i)) : IsVLDisjoint φ (∑ i, ψ i) := by32 classical33 suffices ∀ s : Finset (Fin n), IsVLDisjoint φ (∑ i ∈ s, ψ i) by simpa using this Finset.univ34 intro s35 induction s using Finset.induction_on with36 | empty => simpa using isVLDisjoint_zero_right φ37 | @insert i s hi ih =>38 rw [Finset.sum_insert hi]39 exact (h i).add_right ih4041/-- A disjoint dual family almost attains its total mass on a positive primal42partition. No primal order supremum is taken. -/43lemma exists_partition_mass (n : ℕ) (ψ : Fin n → StrongDual ℝ E)44 (hψ : ∀ i, 0 ≤ ψ i) (hd : Pairwise fun i j => IsVLDisjoint (ψ i) (ψ j))45 (u : E) (hu : 0 ≤ u) (ε : ℝ) (hε : 0 < ε) :46 ∃ y : Fin n → E, (∀ i, 0 ≤ y i) ∧ (∑ i, y i) ≤ u ∧47 (∑ i, ψ i u) - ε < ∑ i, ψ i (y i) := by48 classical49 induction n generalizing u ε with50 | zero => exact ⟨Fin.elim0, fun i => i.elim0, by simpa using hu, by simpa using hε⟩51 | succ n ih =>52 let ψt : Fin n → StrongDual ℝ E := fun i => ψ i.succ53 have hψt : ∀ i, 0 ≤ ψt i := fun i => hψ i.succ54 have hdt : Pairwise fun i j => IsVLDisjoint (ψt i) (ψt j) :=55 fun i j hij => hd (fun h => hij (Fin.succ_injective _ h))56 have hds : IsVLDisjoint (ψ 0) (∑ i, ψt i) := disjoint_dual_sum n (ψ 0) ψt57 (fun i => hd (Fin.succ_ne_zero i).symm)58 have hsum0 : 0 ≤ ∑ i, ψt i := Finset.sum_nonneg fun i _ => hψt i59 obtain ⟨a,b,ha,hb,hab,hm⟩ := dual_sup_approx (ψ 0) (∑ i, ψt i) hu (half_pos hε)60 rw [← add_eq_sup_of_isVLDisjoint_of_nonneg (hψ 0) hsum0 hds] at hm61 obtain ⟨yt,hyt,hytu,hym⟩ := ih ψt hψt hdt b hb (ε/2) (half_pos hε)62 refine ⟨Fin.cons a yt, ?_, ?_, ?_⟩63 · intro i64 exact Fin.cases ha hyt i65 · simpa only [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ] using66 (add_le_add (le_refl a) hytu).trans (le_of_eq hab)67 · simp only [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ]68 change ψ 0 u + ∑ i, ψt i u - ε < ψ 0 a + ∑ i, ψt i (yt i)69 simp only [add_apply, sum_apply] at hm70 linarith7172omit [BanachLattice E] in73lemma partition_pair_le (n : ℕ) (y : Fin n → E) (hy : ∀ i, 0 ≤ y i)74 {u : E} (hs : (∑ i, y i) ≤ u) {i j : Fin n} (hij : i ≠ j) :75 y i + y j ≤ u := by76 classical77 calc78 _ = ∑ k ∈ ({i,j} : Finset (Fin n)), y k := by simp [hij]79 _ ≤ ∑ k, y k := Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _)80 (fun k _ _ => hy k)81 _ ≤ u := hs8283omit [BanachLattice E] in84/-- The positive excess over half the total gives a genuine disjoint family. -/85lemma partition_excess_disjoint (n : ℕ) (y : Fin n → E) (hy : ∀ i, 0 ≤ y i)86 {u : E} (hs : (∑ i, y i) ≤ u) :87 Pairwise fun i j => IsVLDisjoint ((y i + y i - u)⁺) ((y j + y j - u)⁺) := by88 intro i j hij89 have hp := partition_pair_le n y hy hs hij90 have hraw : y i + y i - u ≤ -(y j + y j - u) := by91 have h := add_le_add hp hp92 have heq : (y i+y j)+(y i+y j) = (y i+y i)+(y j+y j) := by abel93 rw [heq] at h94 have ht := sub_le_sub_right (sub_le_sub_right h u) (y j+y j)95 convert ht using 1 <;> abel96 apply (isVLDisjoint_comm.mp (isVLDisjoint_posPart_negPart (y j+y j-u))).mono_left97 rw [abs_of_nonneg (posPart_nonneg _), abs_of_nonneg (negPart_nonneg _)]98 change (y i+y i-u) ⊔ 0 ≤ (-(y j+y j-u)) ⊔ 099 exact sup_le_sup_right hraw 0100101lemma sum_disjoint_dual_apply_le {C : ℝ} (hC : 0 ≤ C)102 (hdis : ∀ (n : ℕ) (x : Fin n → E), (∀ i, 0 ≤ x i) →103 (Pairwise fun i j => IsVLDisjoint (x i) (x j)) → ∑ i, ‖x i‖ ≤ C * ‖∑ i, x i‖)104 (n : ℕ) (ψ : Fin n → StrongDual ℝ E) (hψ : ∀ i, 0 ≤ ψ i)105 (hψn : ∀ i, ‖ψ i‖ ≤ 1) (hd : Pairwise fun i j => IsVLDisjoint (ψ i) (ψ j))106 (u : E) (hu : 0 ≤ u) : ∑ i, ψ i u ≤ C * ‖u‖ := by107 classical108 by_contra! hbad109 let ε := ((∑ i, ψ i u) - C*‖u‖)/4110 have hε : 0 < ε := by dsimp [ε]; linarith111 obtain ⟨y,hy,hys,hm⟩ := exists_partition_mass n ψ hψ hd u hu ε hε112 let z : Fin n → E := fun i => (y i+y i-u)⁺113 have hz (i) : 0 ≤ z i := posPart_nonneg _114 have hyle (i) : y i ≤ u := (Finset.single_le_sum (fun j _ => hy j) (Finset.mem_univ i)).trans hys115 have hzle (i) : z i ≤ u := by116 change (y i+y i-u) ⊔ 0 ≤ u117 apply sup_le _ hu118 exact (sub_le_iff_le_add).mpr (add_le_add (hyle i) (hyle i))119 have hzd : Pairwise fun i j => IsVLDisjoint (z i) (z j) := partition_excess_disjoint n y hy hys120 have hznorm : ‖∑ i, z i‖ ≤ ‖u‖ := norm_le_norm_of_abs_le_abs121 (ComplementedLattice.abs_disjoint_sum_le n z hzd u (fun i => by122 rw [abs_of_nonneg (hz i), abs_of_nonneg hu]; exact hzle i))123 have hzup : (∑ i, ψ i (z i)) ≤ C*‖u‖ := calc124 _ ≤ ∑ i, ‖z i‖ := Finset.sum_le_sum fun i _ => calc125 ψ i (z i) ≤ ‖ψ i (z i)‖ := le_abs_self _126 _ ≤ ‖ψ i‖*‖z i‖ := (ψ i).le_opNorm _127 _ ≤ ‖z i‖ := by simpa using mul_le_mul_of_nonneg_right (hψn i) (norm_nonneg _)128 _ ≤ C*‖∑ i, z i‖ := hdis n z hz hzd129 _ ≤ C*‖u‖ := mul_le_mul_of_nonneg_left hznorm hC130 have hzlow : 2*(∑ i, ψ i (y i)) - ∑ i, ψ i u ≤ ∑ i, ψ i (z i) := by131 simp only [Finset.mul_sum, ← Finset.sum_sub_distrib]132 apply Finset.sum_le_sum133 intro i _134 have h := StrongDual.apply_le_apply_of_nonneg (hψ i) (le_posPart (y i+y i-u))135 simpa only [map_sub, map_add, two_mul] using h136 dsimp [ε] at hm137 linarith138139/-- The norm of a disjoint sum of positive unit dual functionals is controlled140by the primal disjoint lower-one constant. -/141lemma norm_sum_disjoint_dual_le {C : ℝ} (hC : 0 ≤ C)142 (hdis : ∀ (n : ℕ) (x : Fin n → E), (∀ i, 0 ≤ x i) →143 (Pairwise fun i j => IsVLDisjoint (x i) (x j)) → ∑ i, ‖x i‖ ≤ C * ‖∑ i, x i‖)144 (n : ℕ) (ψ : Fin n → StrongDual ℝ E) (hψ : ∀ i, 0 ≤ ψ i)145 (hψn : ∀ i, ‖ψ i‖ ≤ 1) (hd : Pairwise fun i j => IsVLDisjoint (ψ i) (ψ j)) :146 ‖∑ i, ψ i‖ ≤ C := by147 apply ContinuousLinearMap.opNorm_le_bound _ hC148 intro x149 have hsum : 0 ≤ ∑ i, ψ i := Finset.sum_nonneg fun i _ => hψ i150 calc151 _ ≤ (∑ i, ψ i) |x| := StrongDual.abs_apply_le_apply_abs hsum x152 _ = ∑ i, ψ i |x| := sum_apply _ _ _153 _ ≤ C*‖|x|‖ := sum_disjoint_dual_apply_le hC hdis n ψ hψ hψn hd |x| (abs_nonneg x)154 _ = C*‖x‖ := by rw [norm_abs_eq_norm]155156/-- A uniform disjoint lower-one estimate implies the corresponding estimate157for every positive finite family, with exactly the same constant. -/158theorem positiveLowerOne_of_disjoint {C : ℝ} (hC : 0 ≤ C)159 (hdis : ∀ (n : ℕ) (x : Fin n → E), (∀ i, 0 ≤ x i) →160 (Pairwise fun i j => IsVLDisjoint (x i) (x j)) → ∑ i, ‖x i‖ ≤ C * ‖∑ i, x i‖) :161 ALRenorming.PositiveLowerOne (E := E) C := by162 refine ⟨hC, ?_⟩163 intro n x hx164 choose ν hν hνn hνx using fun i => StrongDual.exists_positive_dual_norming (hx i)165 obtain ⟨ψ,hψ,hψle,hψd,hψmaj⟩ :=166 FiniteDualDisjointization.exists_disjoint_majorizing_refinement n ν hν167 have hψn (i) : ‖ψ i‖ ≤ 1 := (norm_le_norm_of_abs_le_abs (by168 rw [abs_of_nonneg (hψ i), abs_of_nonneg (hν i)]169 exact hψle i)).trans (hνn i)170 have hnorm := norm_sum_disjoint_dual_le hC hdis n ψ hψ hψn hψd171 calc172 ∑ i, ‖x i‖ = ∑ i, ν i (x i) := by simp only [hνx]173 _ ≤ ∑ i, (∑ j, ψ j) (x i) := Finset.sum_le_sum fun i _ =>174 StrongDual.le_iff.mp (hψmaj i) (x i) (hx i)175 _ = (∑ j, ψ j) (∑ i, x i) := (map_sum _ _ _).symm176 _ ≤ ‖(∑ j, ψ j) (∑ i, x i)‖ := le_abs_self _177 _ ≤ ‖∑ j, ψ j‖ * ‖∑ i, x i‖ := ContinuousLinearMap.le_opNorm _ _178 _ ≤ C*‖∑ i, x i‖ := mul_le_mul_of_nonneg_right hnorm (norm_nonneg _)179180/-- Uniform finite summing bounds give the positive lower-one estimate. -/181theorem positiveLowerOne_of_summing {C : ℝ} (hC : 0 ≤ C)182 (hOne : ∀ (n : ℕ) (S : E →L[ℝ] EuclideanSpace ℝ (Fin n)),183 ComplementedLattice.OneSummingWith S (C * ‖S‖))184 (hTwo : ∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] E),185 ComplementedLattice.TwoSummingWith T (C * ‖T‖)) :186 ALRenorming.PositiveLowerOne (E := E) (C ^ 2) :=187 positiveLowerOne_of_disjoint (sq_nonneg C)188 (DisjointNormingFunctionals.positive_disjoint_sum_norm_le C hC hOne hTwo)189190/-- The positive lower-one estimate for an actual complemented copy, with all191ambient summing hypotheses explicit and no projection-property premise. -/192theorem positiveLowerOne_of_complemented_ambient193 {Y : Type*} [NormedAddCommGroup Y] [NormedSpace ℝ Y]194 (Q : EnfloStarbird.ComplementedCopy ℝ E Y) {G : ℝ} (hG : 0 ≤ G)195 (hOne : ∀ (n : ℕ) (S : Y →L[ℝ] EuclideanSpace ℝ (Fin n)),196 ComplementedLattice.OneSummingWith S (G * ‖S‖))197 (hTwo : ∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] Y),198 ComplementedLattice.TwoSummingWith T (G * ‖T‖)) :199 ALRenorming.PositiveLowerOne (E := E) ((G * ‖Q.embedding‖ * ‖Q.retraction‖) ^ 2) := by200 obtain ⟨hC, hOneE, hTwoE⟩ := ComplementedLattice.uniform_finite_summing_estimates Q hG hOne hTwo201 exact positiveLowerOne_of_summing hC hOneE hTwoE202203end PL1.PositiveLowerOneBridge204205206207208