PL1/SmoothingApproximation.lean

All source files · Download exact source

SHA-256: 14ea600dbdf2b97c0ce5d7072d3571476c37bb81efdc7d13e6423cc30f9b4851

1import PL1.SmoothingTrace23/-! # Stability of the smoothing trace obstruction under operator-norm limits -/45noncomputable section6set_option autoImplicit false7set_option maxHeartbeats 8000008set_option backward.isDefEq.respectTransparency false9open MeasureTheory Filter10open scoped ENNReal Topology1112namespace PL1.SmoothingTrace1314attribute [local instance] DyadicTrace.intervalMeasure_probability1516variable {𝕜 Ω Ω₂ : Type*} [RCLike 𝕜] [MeasurableSpace Ω] [MeasurableSpace Ω₂]17  (μ : Measure Ω) (ν : Measure Ω₂)1819theorem norm_restricted_sandwich_sub_le20    (A : Lp 𝕜 1 ν →L[𝕜] IntervalL1 𝕜)21    (S T : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)22    (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ) :23    ‖DyadicTrace.restrictLinfty (A.comp (S.comp B) - A.comp (T.comp B))‖ ≤24      (‖A‖ * ‖S - T‖) * ‖OperatorDomination.restriction μ B‖ := by25  have heq : DyadicTrace.restrictLinfty (A.comp (S.comp B) - A.comp (T.comp B)) =26      (A.comp (S - T)).comp (OperatorDomination.restriction μ B) := by27    apply ContinuousLinearMap.ext28    intro f29    simp only [DyadicTrace.restrictLinfty, OperatorDomination.restriction,30      ContinuousLinearMap.comp_apply, sub_apply, map_sub]31  rw [heq]32  exact (ContinuousLinearMap.opNorm_comp_le _ _).trans33    (mul_le_mul_of_nonneg_right (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _))3435theorem trace_tendsto_zero_of_operator_approximation36    (A : Lp 𝕜 1 ν →L[𝕜] IntervalL1 𝕜)37    (S : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)38    (Sₙ : ℕ → Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)39    (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)40    (hS : Tendsto (fun m => ‖S - Sₙ m‖) atTop (𝓝 0))41    (htrace : ∀ m, Tendsto (fun n => DyadicTrace.trace n (A.comp ((Sₙ m).comp B)))42      atTop (𝓝 0)) :43    Tendsto (fun n => DyadicTrace.trace n (A.comp (S.comp B))) atTop (𝓝 0) := by44  apply DyadicTrace.trace_tendsto_zero_of_approximation _45    (fun m => A.comp ((Sₙ m).comp B)) htrace46  apply squeeze_zero (fun m => norm_nonneg _)47    (fun m => norm_restricted_sandwich_sub_le μ ν A S (Sₙ m) B)48  simpa using (hS.const_mul ‖A‖).mul_const ‖OperatorDomination.restriction μ B‖4950variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]5152/-- The exponents of the smoothing approximations may approach one. -/53theorem trace_tendsto_zero_of_smoothing_approximation54    (A : Lp 𝕜 1 ν →L[𝕜] IntervalL1 𝕜)55    (S : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)56    (Sₙ : ℕ → Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)57    (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)58    (hS : Tendsto (fun m => ‖S - Sₙ m‖) atTop (𝓝 0))59    (p : ℕ → ℝ≥0∞) [∀ m, Fact (1 ≤ p m)] (hp2 : ∀ m, p m < 2)60    (Q : ∀ m, Lp 𝕜 (p m) μ →L[𝕜] H) (j : H →L[𝕜] Lp 𝕜 1 ν)61    (hQ : ∀ m (g : Lp 𝕜 1 μ) (f : Lp 𝕜 (p m) μ), g =ᵐ[μ] f → Sₙ m g = j (Q m f)) :62    Tendsto (fun n => DyadicTrace.trace n (A.comp (S.comp B))) atTop (𝓝 0) := by63  apply trace_tendsto_zero_of_operator_approximation μ ν A S Sₙ B hS64  intro m65  exact trace_tendsto_zero_of_smoothing μ ν A (Sₙ m) B (p m) (Fact.out) (hp2 m) (Q m) j (hQ m)6667theorem one_le_norm_id_sub_of_smoothing_approximation68    (A : Lp 𝕜 1 ν →L[𝕜] IntervalL1 𝕜)69    (S : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)70    (Sₙ : ℕ → Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)71    (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)72    (hS : Tendsto (fun m => ‖S - Sₙ m‖) atTop (𝓝 0))73    (p : ℕ → ℝ≥0∞) [∀ m, Fact (1 ≤ p m)] (hp2 : ∀ m, p m < 2)74    (Q : ∀ m, Lp 𝕜 (p m) μ →L[𝕜] H) (j : H →L[𝕜] Lp 𝕜 1 ν)75    (hQ : ∀ m (g : Lp 𝕜 1 μ) (f : Lp 𝕜 (p m) μ), g =ᵐ[μ] f → Sₙ m g = j (Q m f)) :76    1 ≤ ‖DyadicTrace.restrictLinfty77      (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) - A.comp (S.comp B))‖ :=78  DyadicTrace.one_le_norm_id_sub _79    (trace_tendsto_zero_of_smoothing_approximation μ ν A S Sₙ B hS p hp2 Q j hQ)8081end PL1.SmoothingTrace82