PL1/OutputCompression.lean

All source files · Download exact source

SHA-256: aba29497683305f48fa2f56bcd3eafbc5817fd045cda08a7d743371836b10064

1import PL1.MatrixTrace23/-! # Output truncation from summable operator columns45For a fixed finite set of input coordinates, summability of each column's6operator norms gives convergence of output truncations in operator norm.7-/89noncomputable section10set_option backward.isDefEq.respectTransparency false11set_option maxHeartbeats 80000012open Filter13open scoped Topology ENNReal BigOperators1415namespace PL1.OutputCompression1617open MatrixTrace1819variable {𝕜 Y : Type*} [RCLike 𝕜] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]2021/-- The norm omitted by a coordinate truncation is exactly its scalar tail sum. -/22theorem norm_sub_compression_range (N : ℕ) (x : L1Sum Y) :23    ‖x - compression (𝕜 := 𝕜) (Finset.range N) x‖ = ∑' i : ℕ, ‖x (i + N)‖ := by24  rw [compression_apply]25  have h := lp.norm_compl_sum_single (by norm_num : 0 < (1 : ℝ≥0∞).toReal)26    x (Finset.range N)27  simp only [ENNReal.toReal_one, Real.rpow_one] at h28  have ht := (L1Sum.summable_norm x).sum_add_tsum_nat_add N29  rw [← L1Sum.norm_eq_tsum] at ht30  linarith3132/-- An output tail of a single operator column is bounded by its column norm tail. -/33theorem norm_tail_column_le (Q : L1Sum Y →L[𝕜] L1Sum Y) (j : ℕ)34    (hcol : Summable (fun i => ‖entry Q i j‖)) (N : ℕ) :35    ‖(ContinuousLinearMap.id 𝕜 (L1Sum Y) - compression (Finset.range N)).comp36      (Q.comp (insertion j))‖ ≤ ∑' i : ℕ, ‖entry Q (i + N) j‖ := by37  apply ContinuousLinearMap.opNorm_le_bound _ (tsum_nonneg (fun _ => norm_nonneg _))38  intro y39  change ‖Q (insertion j y) - compression (Finset.range N) (Q (insertion j y))‖ ≤ _40  rw [norm_sub_compression_range (𝕜 := 𝕜) N (Q (insertion j y))]41  change (∑' i : ℕ, ‖entry Q (i + N) j y‖) ≤ _42  have hy0 : Summable (fun i : ℕ => ‖entry Q i j y‖) := by43    change Summable (fun i : ℕ => ‖Q (insertion j y) i‖)44    exact L1Sum.summable_norm (Q (insertion j y))45  have hy : Summable (fun i : ℕ => ‖entry Q (i + N) j y‖) :=46    (summable_nat_add_iff N).mpr hy047  have hs : Summable (fun i : ℕ => ‖entry Q (i + N) j‖) :=48    (summable_nat_add_iff N).mpr hcol49  calc50    _ ≤ ∑' i : ℕ, ‖entry Q (i + N) j‖ * ‖y‖ :=51      Summable.tsum_le_tsum (fun i => (entry Q (i + N) j).le_opNorm y) hy (hs.mul_right ‖y‖)52    _ = _ := tsum_mul_right5354/-- Summability is used to bound the actual column, before taking scalar series tails. -/55theorem norm_tail_column_tendsto_zero (Q : L1Sum Y →L[𝕜] L1Sum Y) (j : ℕ)56    (hcol : Summable (fun i => ‖entry Q i j‖)) :57    Tendsto (fun N => ‖(ContinuousLinearMap.id 𝕜 (L1Sum Y) - compression (Finset.range N)).comp58      (Q.comp (insertion j))‖) atTop (𝓝 0) :=59  squeeze_zero (fun _ => norm_nonneg _) (norm_tail_column_le Q j hcol)60    (tendsto_sum_nat_add (fun i => ‖entry Q i j‖))6162/-- Output truncations converge in operator norm after any fixed finite input compression. -/63theorem tendsto_output_compression (Q : L1Sum Y →L[𝕜] L1Sum Y)64    (hcolumns : ∀ j, Summable (fun i => ‖entry Q i j‖)) (F : Finset ℕ) :65    Tendsto (fun N => ‖(ContinuousLinearMap.id 𝕜 (L1Sum Y) - compression (Finset.range N)).comp66      (Q.comp (compression F))‖) atTop (𝓝 0) := by67  let C (N j : ℕ) : Y →L[𝕜] L1Sum Y :=68    (ContinuousLinearMap.id 𝕜 (L1Sum Y) - compression (Finset.range N)).comp69      (Q.comp (insertion j))70  have heq (N : ℕ) :71      (ContinuousLinearMap.id 𝕜 (L1Sum Y) - compression (Finset.range N)).comp72        (Q.comp (compression F)) = ∑ j ∈ F, (C N j).comp (coordinate j) := by73    apply ContinuousLinearMap.ext74    intro x75    simp only [C, compression, ContinuousLinearMap.comp_apply, sub_apply,76      ContinuousLinearMap.id_apply, map_sum, sum_apply]77  have hbound (N : ℕ) :78      ‖(ContinuousLinearMap.id 𝕜 (L1Sum Y) - compression (Finset.range N)).comp79        (Q.comp (compression F))‖ ≤ ∑ j ∈ F, ‖C N j‖ * ‖coordinate (𝕜 := 𝕜) (Y := Y) j‖ := by80    rw [heq]81    exact (norm_sum_le _ _).trans82      (Finset.sum_le_sum (fun j _ => ContinuousLinearMap.opNorm_comp_le _ _))83  apply squeeze_zero (fun _ => norm_nonneg _) hbound84  have h := tendsto_finsetSum F (fun j _ =>85    (norm_tail_column_tendsto_zero Q j (hcolumns j)).mul_const86      ‖coordinate (𝕜 := 𝕜) (Y := Y) j‖)87  simpa only [C, zero_mul, Finset.sum_const_zero] using h8889end PL1.OutputCompression9091