PL1/ResolventEstimates.lean
All source files · Download exact source
SHA-256: 6f5c7d8547ef16d2a0727c5a3f28230acd36bdad0d51869a9803a28574353285
1import PL1.Definitions2import Mathlib.Analysis.SpecificLimits.Basic3import Mathlib.Tactic.FieldSimp4import Mathlib.Tactic.Linarith5import Mathlib.Tactic.NormNum6import Mathlib.Tactic.Positivity7import Mathlib.Tactic.Ring8import Mathlib.Tactic.LinearCombination9import Mathlib.Tactic.Module1011/-!12# Resolvent algebra and the quantitative column estimates1314These lemmas prove the elementary algebra and scalar estimates used in15Propositions 3.2 and 4.2. Operator hypotheses are explicit: this file does not16assert the existence of the product-measure resolvents.17-/1819noncomputable section20set_option maxHeartbeats 80000021open scoped BigOperators2223namespace PL1.ResolventEstimates2425/-- The geometric ratio in the dyadic projection estimates. -/26def dyadicRatio : ℝ := (Real.sqrt 2)⁻¹2728theorem dyadicRatio_pos : 0 < dyadicRatio := by29 unfold dyadicRatio30 positivity3132theorem dyadicRatio_nonneg : 0 ≤ dyadicRatio := dyadicRatio_pos.le3334theorem dyadicRatio_lt_one : dyadicRatio < 1 := by35 have hs : 1 < Real.sqrt 2 := by36 have hp := Real.sqrt_nonneg (2 : ℝ)37 have hsq := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)38 nlinarith39 exact inv_lt_one_of_one_lt₀ hs4041theorem dyadicRatio_sq : dyadicRatio ^ 2 = (1 : ℝ) / 2 := by42 unfold dyadicRatio43 rw [inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]44 norm_num4546theorem dyadicRatio_eq_sqrt_div_two : dyadicRatio = Real.sqrt 2 / 2 := by47 have hs : Real.sqrt 2 ≠ 0 := ne_of_gt (Real.sqrt_pos.2 (by norm_num))48 have hsq := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)49 unfold dyadicRatio50 apply (eq_div_iff (by norm_num : (2 : ℝ) ≠ 0)).251 apply (inv_mul_eq_iff_eq_mul₀ hs).252 nlinarith5354theorem one_sub_dyadicRatio_pos : 0 < 1 - dyadicRatio :=55 sub_pos.2 dyadicRatio_lt_one5657theorem geometric_summable : Summable (fun n : ℕ => dyadicRatio ^ n) :=58 summable_geometric_of_lt_one dyadicRatio_nonneg dyadicRatio_lt_one5960theorem geometric_tsum : (∑' n : ℕ, dyadicRatio ^ n) = (1 - dyadicRatio)⁻¹ :=61 tsum_geometric_of_lt_one dyadicRatio_nonneg dyadicRatio_lt_one6263theorem geometric_tail_summable : Summable (fun n : ℕ => dyadicRatio ^ (n + 1)) := by64 simpa only [pow_succ] using geometric_summable.mul_right dyadicRatio6566theorem geometric_tail_tsum :67 (∑' n : ℕ, dyadicRatio ^ (n + 1)) = dyadicRatio / (1 - dyadicRatio) := by68 simp_rw [pow_succ]69 rw [tsum_mul_right, geometric_tsum]70 ring7172theorem projectionBound_eq :73 (1 + 2 * dyadicRatio) / (1 - dyadicRatio) = PL1.projectionBound := by74 apply (div_eq_iff (ne_of_gt one_sub_dyadicRatio_pos)).275 rw [dyadicRatio_eq_sqrt_div_two, PL1.projectionBound]76 have hsq := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)77 nlinarith7879theorem zeroth_column_bound :80 1 + 2 * (∑' n : ℕ, dyadicRatio ^ (n + 1)) = 3 + 2 * Real.sqrt 2 := by81 rw [geometric_tail_tsum]82 field_simp [ne_of_gt one_sub_dyadicRatio_pos]83 rw [dyadicRatio_eq_sqrt_div_two]84 have hsq := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)85 nlinarith8687theorem zeroth_column_le_projectionBound :88 1 + 2 * (∑' n : ℕ, dyadicRatio ^ (n + 1)) ≤ PL1.projectionBound := by89 rw [zeroth_column_bound, PL1.projectionBound]90 have hs := Real.sqrt_nonneg (2 : ℝ)91 linarith9293theorem column_expression_le (j : ℕ) :94 dyadicRatio ^ (j + 1) +95 2 * (∑ k ∈ Finset.range j, dyadicRatio ^ (k + 1)) +96 (∑' k : ℕ, dyadicRatio ^ k) ≤ PL1.projectionBound := by97 have hp : 0 ≤ dyadicRatio ^ (j + 1) := pow_nonneg dyadicRatio_nonneg _98 have hsum := geometric_tail_summable.sum_le_tsum (Finset.range (j + 1))99 (fun i _ => pow_nonneg dyadicRatio_nonneg (i + 1))100 rw [Finset.sum_range_succ] at hsum101 calc102 _ ≤ 2 * (∑' k : ℕ, dyadicRatio ^ (k + 1)) +103 (∑' k : ℕ, dyadicRatio ^ k) := by linarith104 _ = (1 + 2 * dyadicRatio) / (1 - dyadicRatio) := by105 rw [geometric_tail_tsum, geometric_tsum]106 ring107 _ = PL1.projectionBound := projectionBound_eq108109/-- The column majorant in formula (4.5), with row index first. -/110def majorant : ℕ → ℕ → ℝ111 | 0, 0 => 1112 | i + 1, 0 => 2 * dyadicRatio ^ (i + 1)113 | 0, j + 1 => dyadicRatio ^ (j + 1)114 | i + 1, j + 1 =>115 if i < j then 2 * dyadicRatio ^ (j - i) else dyadicRatio ^ (i - j)116117theorem majorant_nonneg (i j : ℕ) : 0 ≤ majorant i j := by118 rcases i with _ | i <;> rcases j with _ | j <;> simp only [majorant]119 · norm_num120 · exact pow_nonneg dyadicRatio_nonneg _121 · exact mul_nonneg (by norm_num) (pow_nonneg dyadicRatio_nonneg _)122 · split_ifs123 · exact mul_nonneg (by norm_num) (pow_nonneg dyadicRatio_nonneg _)124 · exact pow_nonneg dyadicRatio_nonneg _125126theorem majorant_summable (j : ℕ) : Summable (fun i => majorant i j) := by127 cases j with128 | zero =>129 apply (summable_nat_add_iff 1).1130 simpa only [majorant] using geometric_tail_summable.mul_left 2131 | succ j =>132 apply (summable_nat_add_iff (j + 1)).1133 apply geometric_summable.congr134 intro i135 simp [majorant, Nat.not_lt_of_ge (Nat.le_add_left j i)]136137theorem majorant_zeroth_tsum :138 (∑' i, majorant i 0) = 3 + 2 * Real.sqrt 2 := by139 rw [(majorant_summable 0).tsum_eq_zero_add]140 simp only [majorant, tsum_mul_left]141 exact zeroth_column_bound142143theorem majorant_positive_tsum (j : ℕ) :144 (∑' i, majorant i (j + 1)) = dyadicRatio ^ (j + 1) +145 2 * (∑ k ∈ Finset.range j, dyadicRatio ^ (k + 1)) +146 (∑' k : ℕ, dyadicRatio ^ k) := by147 rw [(majorant_summable (j + 1)).tsum_eq_zero_add]148 have htail : Summable (fun i => majorant (i + 1) (j + 1)) :=149 (summable_nat_add_iff 1).2 (majorant_summable (j + 1))150 rw [← htail.sum_add_tsum_nat_add j]151 have hfinite : (∑ i ∈ Finset.range j, majorant (i + 1) (j + 1)) =152 2 * (∑ k ∈ Finset.range j, dyadicRatio ^ (k + 1)) := by153 rw [Finset.mul_sum]154 rw [← Finset.sum_range_reflect]155 apply Finset.sum_congr rfl156 intro i hi157 have hi' := Finset.mem_range.1 hi158 have hlt : j - 1 - i < j := by omega159 have heq : j - (j - 1 - i) = i + 1 := by omega160 simp [majorant, hlt, heq, mul_comm]161 rw [hfinite]162 have htail_eq : (fun i => majorant (i + j + 1) (j + 1)) =163 (fun i => dyadicRatio ^ i) := by164 funext i165 simp [majorant, Nat.not_lt_of_ge (Nat.le_add_left j i)]166 rw [htail_eq]167 simp only [majorant]168 ring169170theorem majorant_tsum_le (j : ℕ) :171 (∑' i, majorant i j) ≤ PL1.projectionBound := by172 cases j with173 | zero =>174 rw [majorant_zeroth_tsum]175 rw [← zeroth_column_bound]176 exact zeroth_column_le_projectionBound177 | succ j =>178 rw [majorant_positive_tsum]179 exact column_expression_le j180181theorem dyadicRatio_pow_ne_zero (n : ℕ) : dyadicRatio ^ n ≠ 0 :=182 pow_ne_zero n (ne_of_gt dyadicRatio_pos)183184theorem dyadicRatio_sq_pow (n : ℕ) :185 (dyadicRatio ^ 2) ^ n = (dyadicRatio ^ n) ^ 2 := by186 rw [← pow_mul, Nat.mul_comm 2 n, pow_mul]187188theorem dyadicRatio_pow_div {i j : ℕ} (hij : i ≤ j) :189 dyadicRatio ^ j / dyadicRatio ^ i = dyadicRatio ^ (j - i) := by190 apply (div_eq_iff (dyadicRatio_pow_ne_zero i)).2191 rw [← pow_add, Nat.sub_add_cancel hij]192193/-- The estimate for a positive column and a row below its diagonal. -/194theorem weighted_ratio_below_diagonal {i j : ℕ} (hij : i ≤ j) :195 (dyadicRatio ^ (j + 1) / dyadicRatio ^ (i + 1)) *196 (2 * min 1 ((dyadicRatio ^ 2) ^ (i + 1) / (dyadicRatio ^ 2) ^ j)) ≤197 2 * dyadicRatio ^ (j - i) := by198 calc199 _ ≤ (dyadicRatio ^ (j + 1) / dyadicRatio ^ (i + 1)) * (2 * 1) :=200 mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left (min_le_left _ _) (by norm_num))201 (div_nonneg (pow_nonneg dyadicRatio_nonneg _) (pow_nonneg dyadicRatio_nonneg _))202 _ = 2 * dyadicRatio ^ (j - i) := by203 rw [dyadicRatio_pow_div (Nat.add_le_add_right hij 1)]204 simp [Nat.add_sub_add_right, mul_comm]205206/-- Above the diagonal the square of the geometric ratio cancels the factor two. -/207theorem weighted_ratio_above_diagonal {i j : ℕ} (hji : j ≤ i) :208 (dyadicRatio ^ (j + 1) / dyadicRatio ^ (i + 1)) *209 (2 * min 1 ((dyadicRatio ^ 2) ^ (i + 1) / (dyadicRatio ^ 2) ^ j)) ≤210 dyadicRatio ^ (i - j) := by211 calc212 _ ≤ (dyadicRatio ^ (j + 1) / dyadicRatio ^ (i + 1)) *213 (2 * ((dyadicRatio ^ 2) ^ (i + 1) / (dyadicRatio ^ 2) ^ j)) :=214 mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left (min_le_right _ _) (by norm_num))215 (div_nonneg (pow_nonneg dyadicRatio_nonneg _) (pow_nonneg dyadicRatio_nonneg _))216 _ = dyadicRatio ^ (i - j) := by217 rw [dyadicRatio_sq_pow, dyadicRatio_sq_pow]218 rw [pow_succ, pow_succ]219 have hi : dyadicRatio ^ i = dyadicRatio ^ (i - j) * dyadicRatio ^ j := by220 rw [← pow_add, Nat.sub_add_cancel hji]221 rw [hi]222 field_simp [dyadicRatio_pow_ne_zero, ne_of_gt dyadicRatio_pos]223 nlinarith [dyadicRatio_sq]224225/-- The complete scalar estimate for the nonzero rows and columns. -/226theorem weighted_ratio_le_majorant (i j : ℕ) :227 (dyadicRatio ^ (j + 1) / dyadicRatio ^ (i + 1)) *228 (2 * min 1 ((dyadicRatio ^ 2) ^ (i + 1) / (dyadicRatio ^ 2) ^ j)) ≤229 majorant (i + 1) (j + 1) := by230 by_cases hij : i < j231 · simpa only [majorant, ite_eq_left hij] using weighted_ratio_below_diagonal hij.le232 · simpa only [majorant, ite_eq_right hij] using weighted_ratio_above_diagonal (Nat.le_of_not_gt hij)233234/-- The scalar estimate for the zeroth column. -/235theorem weighted_ratio_zero_column (i : ℕ) :236 (dyadicRatio ^ (i + 1))⁻¹ *237 (2 * min 1 ((dyadicRatio ^ 2) ^ (i + 1))) ≤ majorant (i + 1) 0 := by238 calc239 _ ≤ (dyadicRatio ^ (i + 1))⁻¹ * (2 * ((dyadicRatio ^ 2) ^ (i + 1))) :=240 mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left (min_le_right _ _) (by norm_num))241 (inv_nonneg.2 (pow_nonneg dyadicRatio_nonneg _))242 _ = majorant (i + 1) 0 := by243 rw [dyadicRatio_sq_pow, majorant]244 field_simp [dyadicRatio_pow_ne_zero]245246section Operators247248variable {𝕜 Y : Type*} [RCLike 𝕜] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]249250/-- A contraction has defect from the identity of norm at most two. -/251theorem norm_id_sub_le_two (A : Y →L[𝕜] Y) (hA : ‖A‖ ≤ 1) :252 ‖ContinuousLinearMap.id 𝕜 Y - A‖ ≤ 2 := by253 calc254 _ ≤ ‖ContinuousLinearMap.id 𝕜 Y‖ + ‖A‖ := norm_sub_le _ _255 _ ≤ 2 := by linarith [ContinuousLinearMap.norm_id_le (𝕜 := 𝕜) (E := Y)]256257theorem norm_defect_comp_le_two (A B : Y →L[𝕜] Y)258 (hA : ‖A‖ ≤ 1) (hB : ‖B‖ ≤ 1) :259 ‖(ContinuousLinearMap.id 𝕜 Y - A).comp B‖ ≤ 2 := by260 calc261 _ ≤ ‖ContinuousLinearMap.id 𝕜 Y - A‖ * ‖B‖ :=262 ContinuousLinearMap.opNorm_comp_le _ _263 _ ≤ 2 * 1 := mul_le_mul (norm_id_sub_le_two A hA) hB (norm_nonneg _) (by norm_num)264 _ = 2 := by ring265266theorem norm_comp_defect_le_two (A B : Y →L[𝕜] Y)267 (hA : ‖A‖ ≤ 1) (hB : ‖B‖ ≤ 1) :268 ‖A.comp (ContinuousLinearMap.id 𝕜 Y - B)‖ ≤ 2 := by269 calc270 _ ≤ ‖A‖ * ‖ContinuousLinearMap.id 𝕜 Y - B‖ :=271 ContinuousLinearMap.opNorm_comp_le _ _272 _ ≤ 1 * 2 := mul_le_mul hA (norm_id_sub_le_two B hB) (norm_nonneg _) (by norm_num)273 _ = 2 := by ring274275/-- The resolvent identity and contractivity give the estimate in Proposition 3.2.276Taking `c = (s / t : ℝ)` cast into `𝕜` gives the printed bound. -/277theorem norm_defect_comp_le (A B : Y →L[𝕜] Y) (c : 𝕜)278 (hA : ‖A‖ ≤ 1) (hB : ‖B‖ ≤ 1)279 (hres : (ContinuousLinearMap.id 𝕜 Y - A).comp B =280 c • A.comp (ContinuousLinearMap.id 𝕜 Y - B)) :281 ‖(ContinuousLinearMap.id 𝕜 Y - A).comp B‖ ≤ 2 * min 1 ‖c‖ := by282 rw [mul_min_of_nonneg (1 : ℝ) ‖c‖ (by norm_num : (0 : ℝ) ≤ 2)]283 refine le_min ?_ ?_284 · simpa using norm_defect_comp_le_two A B hA hB285 · calc286 _ = ‖c‖ * ‖A.comp (ContinuousLinearMap.id 𝕜 Y - B)‖ := by rw [hres, norm_smul]287 _ ≤ ‖c‖ * 2 := mul_le_mul_of_nonneg_left288 (norm_comp_defect_le_two A B hA hB) (norm_nonneg _)289 _ = 2 * ‖c‖ := mul_comm _ _290291theorem norm_defect_comp_le_real (A B : Y →L[𝕜] Y) (c : ℝ) (hc : 0 ≤ c)292 (hA : ‖A‖ ≤ 1) (hB : ‖B‖ ≤ 1)293 (hres : (ContinuousLinearMap.id 𝕜 Y - A).comp B =294 (c : 𝕜) • A.comp (ContinuousLinearMap.id 𝕜 Y - B)) :295 ‖(ContinuousLinearMap.id 𝕜 Y - A).comp B‖ ≤ 2 * min 1 c := by296 simpa only [RCLike.norm_ofReal, abs_of_nonneg hc] using297 norm_defect_comp_le A B (c : 𝕜) hA hB hres298299/-- The weighted analysis coordinates used to define the intrinsic graph space. -/300def analysisCoordinate (S : ℕ → Y →L[𝕜] Y) : ℕ → Y →L[𝕜] Y301 | 0 => ContinuousLinearMap.id 𝕜 Y302 | n + 1 => (((dyadicRatio ^ (n + 1))⁻¹ : ℝ) : 𝕜) •303 (ContinuousLinearMap.id 𝕜 Y - S (n + 1))304305/-- The columns used to synthesize the retraction. -/306def synthesisCoordinate (S : ℕ → Y →L[𝕜] Y) : ℕ → Y →L[𝕜] Y307 | 0 => S 0308 | n + 1 => ((dyadicRatio ^ (n + 1) : ℝ) : 𝕜) • S n309310theorem synthesisCoordinate_norm_le_one (S : ℕ → Y →L[𝕜] Y)311 (hS : ∀ n, ‖S n‖ ≤ 1) (j : ℕ) : ‖synthesisCoordinate S j‖ ≤ 1 := by312 cases j with313 | zero => exact hS 0314 | succ j =>315 rw [synthesisCoordinate, norm_smul, RCLike.norm_ofReal,316 abs_of_nonneg (pow_nonneg dyadicRatio_nonneg _)]317 calc318 _ ≤ dyadicRatio ^ (j + 1) * 1 :=319 mul_le_mul_of_nonneg_left (hS j) (pow_nonneg dyadicRatio_nonneg _)320 _ ≤ 1 := by simpa using pow_le_one₀ dyadicRatio_nonneg dyadicRatio_lt_one.le321322/-- Every block has the explicit geometric majorant from the paper. -/323theorem weighted_block_norm_le_majorant (S : ℕ → Y →L[𝕜] Y)324 (hS : ∀ n, ‖S n‖ ≤ 1)325 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =326 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •327 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j))328 (i j : ℕ) :329 ‖(analysisCoordinate S i).comp (synthesisCoordinate S j)‖ ≤ majorant i j := by330 cases i with331 | zero =>332 cases j with333 | zero => simpa [analysisCoordinate, synthesisCoordinate, majorant] using hS 0334 | succ j =>335 simp only [analysisCoordinate, synthesisCoordinate, ContinuousLinearMap.id_comp,336 norm_smul, RCLike.norm_ofReal, abs_of_nonneg (pow_nonneg dyadicRatio_nonneg _), majorant]337 simpa using mul_le_mul_of_nonneg_left (hS j) (pow_nonneg dyadicRatio_nonneg (j + 1))338 | succ i =>339 cases j with340 | zero =>341 have hb := norm_defect_comp_le_real (S (i + 1)) (S 0)342 ((dyadicRatio ^ 2) ^ (i + 1)) (pow_nonneg (sq_nonneg _) _)343 (hS (i + 1)) (hS 0) (by simpa using hres (i + 1) 0)344 rw [analysisCoordinate, synthesisCoordinate, ContinuousLinearMap.smul_comp,345 norm_smul, RCLike.norm_ofReal,346 abs_of_nonneg (inv_nonneg.2 (pow_nonneg dyadicRatio_nonneg _))]347 exact (mul_le_mul_of_nonneg_left hb348 (inv_nonneg.2 (pow_nonneg dyadicRatio_nonneg _))).trans (weighted_ratio_zero_column i)349 | succ j =>350 have hc : 0 ≤ (dyadicRatio ^ 2) ^ (i + 1) / (dyadicRatio ^ 2) ^ j :=351 div_nonneg (pow_nonneg (sq_nonneg _) _) (pow_nonneg (sq_nonneg _) _)352 have hb := norm_defect_comp_le_real (S (i + 1)) (S j)353 ((dyadicRatio ^ 2) ^ (i + 1) / (dyadicRatio ^ 2) ^ j) hc354 (hS (i + 1)) (hS j) (hres (i + 1) j)355 rw [analysisCoordinate, synthesisCoordinate, ContinuousLinearMap.smul_comp,356 ContinuousLinearMap.comp_smul, norm_smul, norm_smul,357 RCLike.norm_ofReal, RCLike.norm_ofReal,358 abs_of_nonneg (inv_nonneg.2 (pow_nonneg dyadicRatio_nonneg _)),359 abs_of_nonneg (pow_nonneg dyadicRatio_nonneg _)]360 calc361 _ = (dyadicRatio ^ (j + 1) / dyadicRatio ^ (i + 1)) *362 ‖(ContinuousLinearMap.id 𝕜 Y - S (i + 1)).comp (S j)‖ := by ring363 _ ≤ (dyadicRatio ^ (j + 1) / dyadicRatio ^ (i + 1)) *364 (2 * min 1 ((dyadicRatio ^ 2) ^ (i + 1) / (dyadicRatio ^ 2) ^ j)) :=365 mul_le_mul_of_nonneg_left hb366 (div_nonneg (pow_nonneg dyadicRatio_nonneg _) (pow_nonneg dyadicRatio_nonneg _))367 _ ≤ majorant (i + 1) (j + 1) := weighted_ratio_le_majorant i j368369theorem weighted_block_norm_summable (S : ℕ → Y →L[𝕜] Y)370 (hS : ∀ n, ‖S n‖ ≤ 1)371 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =372 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •373 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (j : ℕ) :374 Summable (fun i => ‖(analysisCoordinate S i).comp (synthesisCoordinate S j)‖) :=375 (majorant_summable j).of_nonneg_of_le (fun _ => norm_nonneg _)376 (fun i => weighted_block_norm_le_majorant S hS hres i j)377378theorem weighted_block_norm_tsum_le (S : ℕ → Y →L[𝕜] Y)379 (hS : ∀ n, ‖S n‖ ≤ 1)380 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =381 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •382 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (j : ℕ) :383 (∑' i, ‖(analysisCoordinate S i).comp (synthesisCoordinate S j)‖) ≤ PL1.projectionBound :=384 (Summable.tsum_le_tsum (fun i => weighted_block_norm_le_majorant S hS hres i j)385 (weighted_block_norm_summable S hS hres j) (majorant_summable j)).trans (majorant_tsum_le j)386387theorem weighted_column_apply_norm_summable (S : ℕ → Y →L[𝕜] Y)388 (hS : ∀ n, ‖S n‖ ≤ 1)389 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =390 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •391 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (j : ℕ) (x : Y) :392 Summable (fun i => ‖analysisCoordinate S i (synthesisCoordinate S j x)‖) := by393 apply ((weighted_block_norm_summable S hS hres j).mul_right ‖x‖).of_nonneg_of_le394 (fun _ => norm_nonneg _)395 intro i396 exact ((analysisCoordinate S i).comp (synthesisCoordinate S j)).le_opNorm x397398/-- A synthesis column maps into the intrinsic graph domain with norm at most C. -/399theorem weighted_column_apply_norm_tsum_le (S : ℕ → Y →L[𝕜] Y)400 (hS : ∀ n, ‖S n‖ ≤ 1)401 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =402 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •403 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (j : ℕ) (x : Y) :404 (∑' i, ‖analysisCoordinate S i (synthesisCoordinate S j x)‖) ≤405 PL1.projectionBound * ‖x‖ := by406 calc407 _ ≤ ∑' i, ‖(analysisCoordinate S i).comp (synthesisCoordinate S j)‖ * ‖x‖ :=408 Summable.tsum_le_tsum409 (fun i => ((analysisCoordinate S i).comp (synthesisCoordinate S j)).le_opNorm x)410 (weighted_column_apply_norm_summable S hS hres j x)411 ((weighted_block_norm_summable S hS hres j).mul_right ‖x‖)412 _ = (∑' i, ‖(analysisCoordinate S i).comp (synthesisCoordinate S j)‖) * ‖x‖ :=413 tsum_mul_right414 _ ≤ PL1.projectionBound * ‖x‖ :=415 mul_le_mul_of_nonneg_right (weighted_block_norm_tsum_le S hS hres j) (norm_nonneg _)416417/-- The half-ratio resolvent identity yields the dyadic telescoping relation. -/418theorem dyadic_telescoping (A B : Y →L[𝕜] Y)419 (hcomm : A.comp B = B.comp A)420 (hres : (ContinuousLinearMap.id 𝕜 Y - B).comp A =421 (2 : 𝕜)⁻¹ • B.comp (ContinuousLinearMap.id 𝕜 Y - A)) :422 A.comp (ContinuousLinearMap.id 𝕜 Y - B) = B - A := by423 ext x424 have h := congrArg (fun T : Y →L[𝕜] Y => T x) hres425 have hc := congrArg (fun T : Y →L[𝕜] Y => T x) hcomm426 simp only [sub_apply, ContinuousLinearMap.comp_apply,427 ContinuousLinearMap.id_apply, smul_apply, map_sub] at h hc ⊢428 rw [hc]429 linear_combination (norm := module) (2 : 𝕜) • h430431/-- Specialization of the resolvent family identity to neighboring dyadic scales. -/432theorem dyadic_family_telescoping (S : ℕ → Y →L[𝕜] Y)433 (hcomm : ∀ i j, (S i).comp (S j) = (S j).comp (S i))434 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =435 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •436 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (n : ℕ) :437 (S n).comp (ContinuousLinearMap.id 𝕜 Y - S (n + 1)) = S (n + 1) - S n := by438 apply dyadic_telescoping (S n) (S (n + 1)) (hcomm n (n + 1))439 have hr : (dyadicRatio ^ 2) ^ (n + 1) / (dyadicRatio ^ 2) ^ n = (1 : ℝ) / 2 := by440 rw [pow_succ, mul_div_cancel_left₀ _ (pow_ne_zero n (dyadicRatio_pow_ne_zero 2))]441 exact dyadicRatio_sq442 simpa only [hr, RCLike.ofReal_div, RCLike.ofReal_inv, RCLike.ofReal_one,443 RCLike.ofReal_ofNat, one_div]444 using hres (n + 1) n445446/-- The weights cancel in each nonzero term of the synthesis-after-analysis map. -/447theorem weighted_composition_telescoping (S : ℕ → Y →L[𝕜] Y)448 (hcomm : ∀ i j, (S i).comp (S j) = (S j).comp (S i))449 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =450 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •451 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (n : ℕ) :452 (synthesisCoordinate S (n + 1)).comp (analysisCoordinate S (n + 1)) =453 S (n + 1) - S n := by454 rw [synthesisCoordinate, analysisCoordinate, ContinuousLinearMap.smul_comp,455 ContinuousLinearMap.comp_smul, smul_smul]456 have hw : ((dyadicRatio ^ (n + 1) : ℝ) : 𝕜) *457 (((dyadicRatio ^ (n + 1))⁻¹ : ℝ) : 𝕜) = 1 := by458 rw [← RCLike.ofReal_mul, mul_inv_cancel₀ (dyadicRatio_pow_ne_zero _), RCLike.ofReal_one]459 rw [hw, one_smul]460 exact dyadic_family_telescoping S hcomm hres n461462/-- Every finite synthesis-after-analysis sum is exactly the last resolvent. -/463theorem weighted_composition_partial_sum (S : ℕ → Y →L[𝕜] Y)464 (hcomm : ∀ i j, (S i).comp (S j) = (S j).comp (S i))465 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =466 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •467 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (N : ℕ) :468 (∑ j ∈ Finset.range (N + 1), (synthesisCoordinate S j).comp (analysisCoordinate S j)) =469 S N := by470 induction N with471 | zero => simp [analysisCoordinate, synthesisCoordinate]472 | succ N ih =>473 rw [Finset.sum_range_succ, ih, weighted_composition_telescoping S hcomm hres N]474 abel475476theorem weighted_composition_partial_sum_apply (S : ℕ → Y →L[𝕜] Y)477 (hcomm : ∀ i j, (S i).comp (S j) = (S j).comp (S i))478 (hres : ∀ i j, (ContinuousLinearMap.id 𝕜 Y - S i).comp (S j) =479 (((dyadicRatio ^ 2) ^ i / (dyadicRatio ^ 2) ^ j : ℝ) : 𝕜) •480 (S i).comp (ContinuousLinearMap.id 𝕜 Y - S j)) (N : ℕ) (y : Y) :481 (∑ j ∈ Finset.range (N + 1), synthesisCoordinate S j (analysisCoordinate S j y)) = S N y := by482 have h := congrArg (fun T : Y →L[𝕜] Y => T y) (weighted_composition_partial_sum S hcomm hres N)483 simpa using h484485end Operators486487/-- The scalar version of the resolvent identity, used on Walsh characters. -/488theorem scalar_resolvent_identity {s t a : ℝ} (hs : 0 < s) (ht : 0 < t)489 (ha : 0 ≤ a) :490 (1 - (1 + s * a)⁻¹) * (1 + t * a)⁻¹ =491 (s / t) * (1 + s * a)⁻¹ * (1 - (1 + t * a)⁻¹) := by492 have hs' : 1 + s * a ≠ 0 := ne_of_gt (by positivity)493 have ht' : 1 + t * a ≠ 0 := ne_of_gt (by positivity)494 field_simp [hs', ht', ne_of_gt ht]495 ring496497end PL1.ResolventEstimates498