PL1/MatrixSmoothing.lean

All source files · Download exact source

SHA-256: b58e040980f9d9f038d222b64a2d3420d40d8aa0b3336af41f1050abd462f5c8

1import PL1.MatrixTraceLimit2import PL1.OutputCompression34/-! # The matrix trace obstruction from summable columns and smoothing entries -/56noncomputable section7set_option autoImplicit false8set_option maxHeartbeats 8000009set_option backward.isDefEq.respectTransparency false10open MeasureTheory Filter11open scoped ENNReal Topology1213namespace PL1.MatrixTrace1415attribute [local instance] DyadicTrace.intervalMeasure_probability1617variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]18  (μ : Measure Ω) [SFinite μ]1920theorem trace_tendsto_zero_of_summable_columns21    (A : L1Sum (Lp 𝕜 1 μ) →L[𝕜] IntervalL1 𝕜)22    (Q : L1Sum (Lp 𝕜 1 μ) →L[𝕜] L1Sum (Lp 𝕜 1 μ))23    (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 μ))24    (hcolumns : ∀ j, Summable (fun i => ‖entry Q i j‖))25    (hentry : ∀ i j, Tendsto (fun n => DyadicTrace.trace n26      ((A.comp (insertion i)).comp ((entry Q i j).comp ((coordinate j).comp B))))27        atTop (𝓝 0)) :28    Tendsto (fun n => DyadicTrace.trace n (A.comp (Q.comp B))) atTop (𝓝 0) :=29  trace_tendsto_zero_of_column_tails μ A Q B30    (OutputCompression.tendsto_output_compression Q hcolumns) hentry3132variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]3334theorem trace_tendsto_zero_of_smoothing_entries35    (A : L1Sum (Lp 𝕜 1 μ) →L[𝕜] IntervalL1 𝕜)36    (Q : L1Sum (Lp 𝕜 1 μ) →L[𝕜] L1Sum (Lp 𝕜 1 μ))37    (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 μ))38    (hcolumns : ∀ j, Summable (fun i => ‖entry Q i j‖))39    (S : ℕ → ℕ → ℕ → Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ)40    (hS : ∀ i j, Tendsto (fun m => ‖entry Q i j - S i j m‖) atTop (𝓝 0))41    (p : ℕ → ℕ → ℕ → ℝ≥0∞) [∀ i j m, Fact (1 ≤ p i j m)]42    (hp2 : ∀ i j m, p i j m < 2)43    (T : ∀ i j m, Lp 𝕜 (p i j m) μ →L[𝕜] H)44    (J : H →L[𝕜] Lp 𝕜 1 μ)45    (hT : ∀ i j m (g : Lp 𝕜 1 μ) (f : Lp 𝕜 (p i j m) μ),46      g =ᵐ[μ] f → S i j m g = J (T i j m f)) :47    Tendsto (fun n => DyadicTrace.trace n (A.comp (Q.comp B))) atTop (𝓝 0) := by48  apply trace_tendsto_zero_of_summable_columns μ A Q B hcolumns49  intro i j50  exact SmoothingTrace.trace_tendsto_zero_of_smoothing_approximation μ μ51    (A.comp (insertion i)) (entry Q i j) (S i j) ((coordinate j).comp B)52    (hS i j) (p i j) (hp2 i j) (T i j) J (hT i j)5354/-- The whole matrix stays at distance at least one from the interval identity55after arbitrary bounded pre- and post-composition. -/56theorem one_le_norm_id_sub_of_smoothing_entries57    (A : L1Sum (Lp 𝕜 1 μ) →L[𝕜] IntervalL1 𝕜)58    (Q : L1Sum (Lp 𝕜 1 μ) →L[𝕜] L1Sum (Lp 𝕜 1 μ))59    (B : IntervalL1 𝕜 →L[𝕜] L1Sum (Lp 𝕜 1 μ))60    (hcolumns : ∀ j, Summable (fun i => ‖entry Q i j‖))61    (S : ℕ → ℕ → ℕ → Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ)62    (hS : ∀ i j, Tendsto (fun m => ‖entry Q i j - S i j m‖) atTop (𝓝 0))63    (p : ℕ → ℕ → ℕ → ℝ≥0∞) [∀ i j m, Fact (1 ≤ p i j m)]64    (hp2 : ∀ i j m, p i j m < 2)65    (T : ∀ i j m, Lp 𝕜 (p i j m) μ →L[𝕜] H)66    (J : H →L[𝕜] Lp 𝕜 1 μ)67    (hT : ∀ i j m (g : Lp 𝕜 1 μ) (f : Lp 𝕜 (p i j m) μ),68      g =ᵐ[μ] f → S i j m g = J (T i j m f)) :69    1 ≤ ‖DyadicTrace.restrictLinfty70      (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) - A.comp (Q.comp B))‖ :=71  DyadicTrace.one_le_norm_id_sub _72    (trace_tendsto_zero_of_smoothing_entries μ A Q B hcolumns S hS p hp2 T J hT)7374end PL1.MatrixTrace75