PL1/ComplementedLatticeBandEstimates.lean
All source files · Download exact source
SHA-256: ce845022485a2014b3be76d48f119a4e9bf389ffa1c93d9a21203b458bd8de1a
1import PL1.ComplementedLatticeSumming2import PL1.AtomicBandDecomposition34/-! # The finite-band estimate in the AL-renorming argument56This proves the norm estimate underlying Proposition 2.1 of de Hevia et al.7from explicitly quantified 1- and 2-summing estimates. Those deep estimates8are mathematical premises here, not axioms or implicit instances.9-/1011noncomputable section12open scoped BigOperators1314namespace PL1.ComplementedLattice15open AtomicBandDecomposition1617variable {E : Type*} [NormedAddCommGroup E] [Lattice E]18 [IsOrderedAddMonoid E] [NormedVectorLattice E]1920theorem disjoint_of_mem_generated {a b y z : E} (hab : IsVLDisjoint a b)21 (hy : y ∈ Band.generated ({a} : Set E)) (hz : z ∈ Band.generated ({b} : Set E)) :22 IsVLDisjoint y z := by23 have hb : Band.generated ({b} : Set E) ≤ Band.disjointComplement ({a} : Set E) := by24 apply Band.generated_le25 intro t ht s hs26 have ht' : t = b := Set.mem_singleton_iff.mp ht27 have hs' : s = a := Set.mem_singleton_iff.mp hs28 rw [ht', hs']29 exact isVLDisjoint_comm.mpr hab30 have ha : Band.generated ({a} : Set E) ≤31 Band.disjointComplement (Band.generated ({b} : Set E) : Set E) := by32 apply Band.generated_le33 intro t ht s hs34 have ht' : t = a := Set.mem_singleton_iff.mp ht35 rw [ht']36 exact isVLDisjoint_comm.mpr (hb hs a (Set.mem_singleton a))37 exact ha hy z hz3839/-- An arbitrary finite disjoint family dominated in modulus has its entire40sum dominated by the same modulus. -/41theorem abs_disjoint_sum_le (n : ℕ) (y : Fin n → E)42 (hy : Pairwise fun i j => IsVLDisjoint (y i) (y j))43 (z : E) (hz : ∀ i, |y i| ≤ |z|) : |∑ i, y i| ≤ |z| := by44 have habs : Pairwise fun i j => IsVLDisjoint |y i| |y j| := by45 intro i j hij46 simpa only [IsVLDisjoint, abs_abs] using hy hij47 have hsum : |∑ i, y i| = ∑ i, |y i| := by48 simpa only [one_smul, abs_one] using49 (abs_sum_of_pairwise_isVLDisjoint (α := fun _ => (1 : ℝ)) hy)50 rw [hsum]51 by_cases hn : n = 052 · subst n53 simpa using abs_nonneg z54 rw [sum_eq_sup_of_pairwise_isVLDisjoint_of_nonneg (Nat.pos_of_ne_zero hn)55 (fun i => abs_nonneg (y i)) habs]56 exact Finset.sup'_le _ _ (fun i _ => hz i)5758theorem norm_sum_band_projections_le (n : ℕ) (B : Fin n → ProjectionBand E)59 (hB : ∀ i j, i ≠ j → ∀ y ∈ B i, ∀ z ∈ B j, IsVLDisjoint y z) (x : E) :60 ‖∑ i, projection (B i) x‖ ≤ ‖x‖ := by61 apply norm_le_norm_of_abs_le_abs62 apply abs_disjoint_sum_le n _63 · intro i j hij64 exact hB i j hij _ (projection_mem _ _) _ (projection_mem _ _)65 · intro i66 exact (Positive.abs_le_map_abs67 (Positive.zero_le_iff.mp (B i).bandProjection_nonneg) x).trans68 (Positive.le_iff.mp (B i).bandProjection_le_id _ (abs_nonneg x))6970def bandCoordinates (n : ℕ) (B : Fin n → ProjectionBand E)71 (φ : Fin n → E →L[ℝ] ℝ) : E →L[ℝ] EuclideanSpace ℝ (Fin n) :=72 (EuclideanSpace.equiv (Fin n) ℝ).symm.toContinuousLinearMap.comp73 (ContinuousLinearMap.pi (fun i => (φ i).comp (projection (B i))))7475@[simp] theorem bandCoordinates_apply (n : ℕ) (B : Fin n → ProjectionBand E)76 (φ : Fin n → E →L[ℝ] ℝ) (x : E) (i : Fin n) :77 bandCoordinates n B φ x i = φ i (projection (B i) x) := rfl7879theorem norm_bandCoordinates_le (C : ℝ) (hC : 0 ≤ C)80 (hTwo : ∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] E), TwoSummingWith T (C * ‖T‖))81 (n : ℕ) (B : Fin n → ProjectionBand E)82 (hB : ∀ i j, i ≠ j → ∀ y ∈ B i, ∀ z ∈ B j, IsVLDisjoint y z)83 (φ : Fin n → E →L[ℝ] ℝ) (hφ : ∀ i, ‖φ i‖ ≤ 1) :84 ‖bandCoordinates n B φ‖ ≤ C := by85 apply ContinuousLinearMap.opNorm_le_bound _ hC86 intro x87 apply (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hC (norm_nonneg x))).mp88 rw [EuclideanSpace.real_norm_sq_eq]89 have hd : Pairwise fun i j => IsVLDisjoint (projection (B i) x) (projection (B j) x) := by90 intro i j hij91 exact hB i j hij _ (projection_mem _ _) _ (projection_mem _ _)92 let T := disjointSynthesis n (fun i => projection (B i) x) hd93 have hT : ‖T‖ ≤ ‖x‖ :=94 (norm_disjointSynthesis_le n _ hd).trans (norm_sum_band_projections_le n B hB x)95 calc96 _ ≤ ∑ i, ‖projection (B i) x‖ ^ 2 := by97 apply Finset.sum_le_sum98 intro i _99 change (φ i (projection (B i) x)) ^ 2 ≤ _100 have h := (φ i).le_of_opNorm_le (hφ i) (projection (B i) x)101 simpa only [one_mul, Real.norm_eq_abs, sq_abs] using102 pow_le_pow_left₀ (norm_nonneg _) h 2103 _ ≤ (C * ‖T‖) ^ 2 := disjoint_square_sum_le_of_twoSumming n _ hd (hTwo n T)104 _ ≤ (C * ‖x‖) ^ 2 :=105 pow_le_pow_left₀ (mul_nonneg hC (norm_nonneg T))106 (mul_le_mul_of_nonneg_left hT hC) 2107108theorem disjoint_sum_norm_le_of_summing_estimates109 [HasPrincipalProjectionProperty E] (C : ℝ) (hC : 0 ≤ C)110 (hOne : ∀ (n : ℕ) (S : E →L[ℝ] EuclideanSpace ℝ (Fin n)),111 OneSummingWith S (C * ‖S‖))112 (hTwo : ∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] E),113 TwoSummingWith T (C * ‖T‖))114 (n : ℕ) (x : Fin n → E)115 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :116 ∑ i, ‖x i‖ ≤ C ^ 2 * ‖∑ i, x i‖ := by117 classical118 choose B hB using fun i : Fin n =>119 HasPrincipalProjectionProperty.exists_projectionBand (x i)120 have hBdisj : ∀ i j, i ≠ j → ∀ y ∈ B i, ∀ z ∈ B j, IsVLDisjoint y z := by121 intro i j hij y hy z hz122 exact disjoint_of_mem_generated (hx hij)123 (by change y ∈ (B i : Set E) at hy; rw [hB i] at hy; exact hy)124 (by change z ∈ (B j : Set E) at hz; rw [hB j] at hz; exact hz)125 choose φ hφ hφx using fun i : Fin n => exists_dual_vector'' ℝ (x i)126 let S := bandCoordinates n B φ127 have hS : ‖S‖ ≤ C := norm_bandCoordinates_le C hC hTwo n B hBdisj φ hφ128 have hnorm (i : Fin n) : ‖x i‖ ≤ ‖S (x i)‖ := by129 have hmem : x i ∈ B i := by130 change x i ∈ (B i : Set E)131 rw [show (B i : Set E) = (Band.generated ({x i} : Set E) : Set E) from hB i]132 exact Band.subset_generated _ (Set.mem_singleton _)133 have hcoord : S (x i) i = ‖x i‖ := by134 change φ i (projection (B i) (x i)) = ‖x i‖135 rw [projection_eq_self _ hmem]136 simpa using hφx i137 have h := PiLp.norm_apply_le (S (x i)) i138 simpa only [hcoord, Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)] using h139 calc140 _ ≤ ∑ i, ‖S (x i)‖ := Finset.sum_le_sum (fun i _ => hnorm i)141 _ ≤ (C * ‖S‖) * ‖∑ i, x i‖ := (hOne n S).disjoint_sum_le n x hx142 _ ≤ C ^ 2 * ‖∑ i, x i‖ := by143 rw [pow_two]144 exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hS hC) (norm_nonneg _)145146#print axioms disjoint_sum_norm_le_of_summing_estimates147148end PL1.ComplementedLattice149