PL1/NoiseTraceObstruction.lean

All source files · Download exact source

SHA-256: ec2c224d388a5e78bfc3ab44c62ae9cc3c936cb3f347bf5267f6d7daf20f5fda

1import PL1.TruncatedResolventFactorization2import PL1.TraceVanishing34/-!5# From genuine noise smoothing to the actual projection trace obstruction67Only compatible Lp-to-L2 noise extensions are explicit premises here. All8resolvent cutoffs, matrix entries, column summability and approximation limits9are discharged for the actual construction. The missing Enflo-Starbird10subspace theorem is not asserted or assumed by the factorization obstruction.11-/1213noncomputable section14open MeasureTheory Filter15open scoped ENNReal NNReal Topology1617namespace PL1.Noise18open Walsh ResolventEstimates1920variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)2122theorem resolvent_hasVanishingDyadicTrace_of_noise_smoothing23    (t : PositiveTime) (ε : ℕ → ℝ≥0)24    (hε : Tendsto (fun m => (ε m : ℝ)) atTop (𝓝 0))25    (p : ℕ → ℝ≥0∞) [∀ m, Fact (1 ≤ p m)] (hp2 : ∀ m, p m < 2)26    (H : ∀ m, Lp 𝕜 (p m) haar →L[𝕜] Lp 𝕜 2 haar)27    (hH : ∀ m (g : Lp 𝕜 1 haar) (f : Lp 𝕜 (p m) haar),28      g =ᵐ[haar] f → noiseL1 𝕜 rates (ε m) g = l2ToL1 (H m f)) :29    HasVanishingDyadicTrace (resolventL1 𝕜 rates t) := by30  intro A B31  apply SmoothingTrace.trace_tendsto_zero_of_smoothing_approximation haar haar32    A (resolventL1 𝕜 rates t) (fun m => truncatedResolventL1 𝕜 rates t (ε m)) B33    _ p hp2 (fun m => truncatedResolventLpToL2 (rates := rates) t (ε m) (H m)) l2ToL134    (fun m => truncatedResolventLpToL2_overlap t (ε m) (H m) (hH m))35  simpa only [norm_sub_rev] using tendsto_iff_norm_sub_tendsto_zero.mp36    (truncatedResolventL1_tendsto 𝕜 rates atTop t ε hε)3738/-- The matrix entries computed from the actual projection are the original39weighted analysis/reconstruction blocks. -/40theorem projection_entry (i j : ℕ) :41    MatrixTrace.entry (projection 𝕜 rates) i j =42      ((dyadicSystem 𝕜 rates).analysis i).comp ((dyadicSystem 𝕜 rates).baseColumn j) := by43  apply ContinuousLinearMap.ext44  intro f45  change (projection 𝕜 rates) (lp.single 1 j f) i = _46  exact (dyadicSystem 𝕜 rates).projection_single_coord i j f4748theorem projection_summable_column_norms (j : ℕ) :49    Summable (fun i => ‖MatrixTrace.entry (projection 𝕜 rates) i j‖) := by50  simp only [projection_entry]51  exact weighted_block_norm_summable (dyadicSystem 𝕜 rates).operator52    (dyadicSystem 𝕜 rates).contractive (dyadicSystem 𝕜 rates).resolvent j5354theorem projection_entry_hasVanishingDyadicTrace55    (hR : ∀ t : PositiveTime, HasVanishingDyadicTrace (resolventL1 𝕜 rates t))56    (i j : ℕ) : HasVanishingDyadicTrace (MatrixTrace.entry (projection 𝕜 rates) i j) := by57  rw [projection_entry]58  apply HasVanishingDyadicTrace.comp_left59  cases j with60  | zero => exact hR (dyadicTime 0)61  | succ j => exact (hR (dyadicTime j)).smul _6263theorem projection_hasVanishingDyadicTrace_of_resolvents64    (hR : ∀ t : PositiveTime, HasVanishingDyadicTrace (resolventL1 𝕜 rates t)) :65    HasVanishingDyadicTrace (projection 𝕜 rates) := by66  intro A B67  apply MatrixTrace.trace_tendsto_zero_of_summable_columns haar A (projection 𝕜 rates) B68    (projection_summable_column_norms 𝕜 rates)69  intro i j70  exact projection_entry_hasVanishingDyadicTrace 𝕜 rates hR i j71    (A.comp (MatrixTrace.insertion i)) ((MatrixTrace.coordinate j).comp B)7273theorem projection_hasVanishingDyadicTrace_of_noise_smoothing74    (ε : ℕ → ℝ≥0) (hε : Tendsto (fun m => (ε m : ℝ)) atTop (𝓝 0))75    (p : ℕ → ℝ≥0∞) [∀ m, Fact (1 ≤ p m)] (hp2 : ∀ m, p m < 2)76    (H : ∀ m, Lp 𝕜 (p m) haar →L[𝕜] Lp 𝕜 2 haar)77    (hH : ∀ m (g : Lp 𝕜 1 haar) (f : Lp 𝕜 (p m) haar),78      g =ᵐ[haar] f → noiseL1 𝕜 rates (ε m) g = l2ToL1 (H m f)) :79    HasVanishingDyadicTrace (projection 𝕜 rates) :=80  projection_hasVanishingDyadicTrace_of_resolvents 𝕜 rates81    (fun t => resolvent_hasVanishingDyadicTrace_of_noise_smoothing 𝕜 rates t ε hε p hp2 H hH)8283end PL1.Noise84