PL1/MatrixTraceLimit.lean

All source files · Download exact source

SHA-256: bea469326969450106350fee37899de306e852e3f665be64bb2aac325144114f

1import PL1.InputCompression23/-! # Passage from finite matrix traces to the whole operator -/45noncomputable section6set_option autoImplicit false7set_option maxHeartbeats 8000008set_option backward.isDefEq.respectTransparency false9open MeasureTheory Filter10open scoped ENNReal BigOperators Topology1112namespace PL1.MatrixTrace1314attribute [local instance] DyadicTrace.intervalMeasure_probability1516variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]17  (μ : Measure Ω) [SFinite μ]1819theorem trace_tendsto_zero_of_column_tails20    (A : L1Sum (Lp 𝕜 1 μ) →L[𝕜] IntervalL1 𝕜)21    (Q : L1Sum (Lp 𝕜 1 μ) →L[𝕜] L1Sum (Lp 𝕜 1 μ))22    (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 μ))23    (houtput : ∀ F : Finset ℕ, Tendsto (fun m =>24      ‖(ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) - compression (Finset.range m)).comp25        (Q.comp (compression F))‖) atTop (𝓝 0))26    (hentry : ∀ i j, Tendsto (fun n => DyadicTrace.trace n27      ((A.comp (insertion i)).comp ((entry Q i j).comp ((coordinate j).comp B))))28        atTop (𝓝 0)) :29    Tendsto (fun n => DyadicTrace.trace n (A.comp (Q.comp B))) atTop (𝓝 0) := by30  let R (F : Finset ℕ) := A.comp (Q.comp ((compression F).comp B))31  have htrace (F : Finset ℕ) : Tendsto (fun n => DyadicTrace.trace n (R F)) atTop (𝓝 0) := by32    let Rm (m : ℕ) := A.comp ((compression (Finset.range m)).comp (Q.comp ((compression F).comp B)))33    have hRm (m : ℕ) : Tendsto (fun n => DyadicTrace.trace n (Rm m)) atTop (𝓝 0) :=34      compressed_trace_tendsto_zero (Finset.range m) F A Q B (fun i _ j _ => hentry i j)35    apply DyadicTrace.trace_tendsto_zero_of_approximation (R F) Rm hRm36    have heq (m : ℕ) : DyadicTrace.restrictLinfty (R F - Rm m) =37        (A.comp ((ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) - compression (Finset.range m)).comp38          (Q.comp (compression F)))).comp39            (B.comp (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)) := by40      apply ContinuousLinearMap.ext41      intro f42      simp only [R, Rm, DyadicTrace.restrictLinfty, ContinuousLinearMap.comp_apply,43        sub_apply, map_sub, ContinuousLinearMap.id_apply]44    have hn (m : ℕ) : ‖DyadicTrace.restrictLinfty (R F - Rm m)‖ ≤45        (‖A‖ * ‖(ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) - compression (Finset.range m)).comp46          (Q.comp (compression F))‖) * ‖B.comp (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)‖ := by47      rw [heq]48      exact (ContinuousLinearMap.opNorm_comp_le _ _).trans49        (mul_le_mul_of_nonneg_right (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _))50    apply squeeze_zero (fun m => norm_nonneg _) hn51    simpa using ((houtput F).const_mul ‖A‖).mul_const52      ‖B.comp (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)‖53  apply DyadicTrace.trace_tendsto_zero_of_approximation _ (fun n => R (Finset.range n))54    (fun n => htrace (Finset.range n))55  have heq (n : ℕ) : DyadicTrace.restrictLinfty (A.comp (Q.comp B) - R (Finset.range n)) =56      (A.comp Q).comp57        (((ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) - compression (Finset.range n)).comp B).comp58          (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)) := by59    apply ContinuousLinearMap.ext60    intro f61    simp only [R, DyadicTrace.restrictLinfty, ContinuousLinearMap.comp_apply,62      sub_apply, map_sub, ContinuousLinearMap.id_apply]63  have hn (n : ℕ) : ‖DyadicTrace.restrictLinfty (A.comp (Q.comp B) - R (Finset.range n))‖ ≤64      ‖A.comp Q‖ * ‖((ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) - compression (Finset.range n)).comp B).comp65        (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)‖ := by66    rw [heq]67    exact ContinuousLinearMap.opNorm_comp_le _ _68  apply squeeze_zero (fun n => norm_nonneg _) hn69  simpa using (InputCompression.norm_input_compression_error_tendsto_zero μ B).const_mul ‖A.comp Q‖7071theorem one_le_norm_id_sub_of_column_tails72    (A : L1Sum (Lp 𝕜 1 μ) →L[𝕜] IntervalL1 𝕜)73    (Q : L1Sum (Lp 𝕜 1 μ) →L[𝕜] L1Sum (Lp 𝕜 1 μ))74    (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 μ))75    (houtput : ∀ F : Finset ℕ, Tendsto (fun m =>76      ‖(ContinuousLinearMap.id 𝕜 (L1Sum (Lp 𝕜 1 μ)) - compression (Finset.range m)).comp77        (Q.comp (compression F))‖) atTop (𝓝 0))78    (hentry : ∀ i j, Tendsto (fun n => DyadicTrace.trace n79      ((A.comp (insertion i)).comp ((entry Q i j).comp ((coordinate j).comp B))))80        atTop (𝓝 0)) :81    1 ≤ ‖DyadicTrace.restrictLinfty82      (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) - A.comp (Q.comp B))‖ :=83  DyadicTrace.one_le_norm_id_sub _ (trace_tendsto_zero_of_column_tails μ A Q B houtput hentry)8485end PL1.MatrixTrace86