PL1/MatrixTrace.lean

All source files · Download exact source

SHA-256: d9ebf2f0fbcefef57065384d3198913a2cdb0370b1ab6352424eb626153f46c4

1import PL1.SmoothingApproximation2import PL1.L1Sum34/-! # Finite matrix compressions and the interval identity obstruction -/56noncomputable section7set_option autoImplicit false8set_option maxHeartbeats 8000009set_option backward.isDefEq.respectTransparency false10open MeasureTheory Filter11open scoped ENNReal BigOperators Topology1213namespace PL1.MatrixTrace1415attribute [local instance] DyadicTrace.intervalMeasure_probability1617variable {𝕜 Y : Type*} [RCLike 𝕜] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]1819theorem trace_sum {ι : Type*} (s : Finset ι)20    (R : ι → IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) (n : ℕ) :21    DyadicTrace.trace n (∑ i ∈ s, R i) = ∑ i ∈ s, DyadicTrace.trace n (R i) := by22  simp only [DyadicTrace.trace, TraceBounds.partitionTrace, TraceBounds.finiteTrace,23    ContinuousLinearMap.comp_apply, sum_apply, map_sum]24  exact Finset.sum_comm2526theorem trace_tendsto_zero_sum {ι : Type*} (s : Finset ι)27    (R : ι → IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)28    (hR : ∀ i ∈ s, Tendsto (fun n => DyadicTrace.trace n (R i)) atTop (𝓝 0)) :29    Tendsto (fun n => DyadicTrace.trace n (∑ i ∈ s, R i)) atTop (𝓝 0) := by30  simp_rw [trace_sum]31  simpa using tendsto_finsetSum s hR3233def insertion (i : ℕ) : Y →L[𝕜] L1Sum Y :=34  lp.singleContinuousLinearMap 𝕜 (fun _ : ℕ => Y) 1 i3536def coordinate (i : ℕ) : L1Sum Y →L[𝕜] Y :=37  lp.evalCLM 𝕜 (fun _ : ℕ => Y) 1 i3839/-- The actual finite coordinate mask of an ell1 sum. -/40def compression (s : Finset ℕ) : L1Sum Y →L[𝕜] L1Sum Y :=41  ∑ i ∈ s, (insertion (𝕜 := 𝕜) i).comp (coordinate i)4243theorem compression_apply (s : Finset ℕ) (x : L1Sum Y) :44    compression (𝕜 := 𝕜) s x = ∑ i ∈ s, lp.single 1 i (x i) := by45  simp only [compression, sum_apply, ContinuousLinearMap.comp_apply, insertion, coordinate]46  rfl4748theorem compression_apply_coord (s : Finset ℕ) (x : L1Sum Y) (i : ℕ) :49    compression (𝕜 := 𝕜) s x i = if i ∈ s then x i else 0 := by50  rw [compression_apply]51  simp only [lp.coeFn_sum, Finset.sum_apply, lp.coeFn_single, Finset.sum_pi_single]5253theorem norm_compression_le_one (s : Finset ℕ) : ‖compression (𝕜 := 𝕜) (Y := Y) s‖ ≤ 1 := by54  apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one55  intro x56  rw [one_mul, compression_apply]57  have h := lp.norm_compl_sum_single (by norm_num : 0 < (1 : ℝ≥0∞).toReal) x s58  have hc := lp.norm_sum_single (by norm_num : 0 < (1 : ℝ≥0∞).toReal) (fun i => x i) s59  simp only [ENNReal.toReal_one, Real.rpow_one] at h hc60  rw [hc]61  have hn := norm_nonneg (x - ∑ i ∈ s, lp.single 1 i (x i))62  linarith6364def entry (Q : L1Sum Y →L[𝕜] L1Sum Y) (i j : ℕ) : Y →L[𝕜] Y :=65  (coordinate i).comp (Q.comp (insertion j))6667theorem compressed_sandwich_eq_sum (E F : Finset ℕ)68    (A : L1Sum Y →L[𝕜] IntervalL1 𝕜) (Q : L1Sum Y →L[𝕜] L1Sum Y)69    (B : IntervalL1 𝕜 →L[𝕜] L1Sum Y) :70    A.comp ((compression E).comp (Q.comp ((compression F).comp B))) =71      ∑ i ∈ E, ∑ j ∈ F, (A.comp (insertion i)).comp72        ((entry Q i j).comp ((coordinate j).comp B)) := by73  apply ContinuousLinearMap.ext74  intro f75  simp only [compression, entry, ContinuousLinearMap.comp_apply, sum_apply, map_sum]76  exact Finset.sum_comm7778theorem compressed_trace_tendsto_zero (E F : Finset ℕ)79    (A : L1Sum Y →L[𝕜] IntervalL1 𝕜) (Q : L1Sum Y →L[𝕜] L1Sum Y)80    (B : IntervalL1 𝕜 →L[𝕜] L1Sum Y)81    (hentry : ∀ i ∈ E, ∀ j ∈ F, Tendsto (fun n => DyadicTrace.trace n82      ((A.comp (insertion i)).comp ((entry Q i j).comp ((coordinate j).comp B))))83        atTop (𝓝 0)) :84    Tendsto (fun n => DyadicTrace.trace n85      (A.comp ((compression E).comp (Q.comp ((compression F).comp B))))) atTop (𝓝 0) := by86  rw [compressed_sandwich_eq_sum]87  apply trace_tendsto_zero_sum88  intro i hi89  exact trace_tendsto_zero_sum F _ (hentry i hi)9091theorem one_le_norm_id_sub_compression (E F : Finset ℕ)92    (A : L1Sum Y →L[𝕜] IntervalL1 𝕜) (Q : L1Sum Y →L[𝕜] L1Sum Y)93    (B : IntervalL1 𝕜 →L[𝕜] L1Sum Y)94    (hentry : ∀ i ∈ E, ∀ j ∈ F, Tendsto (fun n => DyadicTrace.trace n95      ((A.comp (insertion i)).comp ((entry Q i j).comp ((coordinate j).comp B))))96        atTop (𝓝 0)) :97    1 ≤ ‖DyadicTrace.restrictLinfty (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) -98      A.comp ((compression E).comp (Q.comp ((compression F).comp B))))‖ :=99  DyadicTrace.one_le_norm_id_sub _ (compressed_trace_tendsto_zero E F A Q B hentry)100101end PL1.MatrixTrace102