On complemented subspaces of L1[0,1]L_1[0,1]

PL1/SmoothingTrace.lean

All source files · Download exact source

SHA-256: 55a777e25c00550a8f7c0c18245312cd7ddc2d0459128c283be8a89155c010f1

1import PL1.HilbertDyadicTrace2import PL1.DyadicCellMeasure3import PL1.LpOperatorLift45/-! # Trace vanishing for operators with an Lp-to-Hilbert smoothing extension -/67noncomputable section8set_option autoImplicit false9set_option maxHeartbeats 80000010set_option backward.isDefEq.respectTransparency false11open MeasureTheory Filter12open scoped ENNReal BigOperators Topology1314namespace PL1.SmoothingTrace1516attribute [local instance] DyadicTrace.intervalMeasure_probability1718variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω] (μ : Measure Ω)1920theorem norm_cellVector_le_one (n i : ℕ) :21    ‖HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i‖ ≤ 1 := by22  have h := norm_indicatorConstLp_le (p := ∞) (hs := DyadicTrace.measurableSet_cell n i)23    (hμs := measure_ne_top intervalMeasure (DyadicTrace.cell n i)) (c := (1 : 𝕜))24  simpa only [HilbertDyadicTrace.cellVector, TraceBounds.cellVector,25    ENNReal.toReal_top, div_zero, Real.rpow_zero, norm_one, mul_one] using h2627theorem norm_inclusion_cellVector (n i : ℕ) (hi : i < 2 ^ n) :28    ‖ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top29      (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i)‖ = ((2 : ℝ) ^ n)⁻¹ := by30  rw [TraceBounds.inclusion_cellVector, norm_indicatorConstLp (by norm_num) (by norm_num)]31  simp only [norm_one, ENNReal.toReal_one, div_one, Real.rpow_one, one_mul,32    measureReal_def, DyadicTrace.intervalMeasure_cell_toReal n i hi]3334variable (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ) (G : Ω → ℝ) (hG : Measurable G)35  (hdom : ∀ f : Lp 𝕜 ∞ intervalMeasure, ‖f‖ ≤ 1 →36    ∀ᵐ x ∂μ, ‖OperatorDomination.restriction μ B f x‖ ≤ G x)3738theorem norm_maskedRestriction_cell_le (M : ℝ) (n i : ℕ) (hi : i < 2 ^ n) :39    ‖OperatorDomination.maskedRestriction μ B G hG M40      (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i)‖ ≤ ‖B‖ * ((2 : ℝ) ^ n)⁻¹ := by41  have hmask := L1Masks.norm_maskFun_le μ {x | G x ≤ M}42    (measurableSet_le hG measurable_const)43    (OperatorDomination.restriction μ B (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i))44  change ‖OperatorDomination.maskedRestriction μ B G hG M45    (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i)‖ ≤ _ at hmask46  exact hmask.trans ((B.le_opNorm _).trans_eq47    (congrArg (fun z : ℝ => ‖B‖ * z) (norm_inclusion_cellVector (𝕜 := 𝕜) n i hi)))4849theorem norm_maskedRestrictionLp_cell_le (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞)50    [Fact (1 ≤ p)] (M : ℝ) (hM : 0 ≤ M) (n i : ℕ) (hi : i < 2 ^ n) :51    ‖OperatorDomination.maskedRestrictionLp μ B G hG hdom p hp hptop M hM52      (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i)‖ ≤53      (M ^ (1 - 1 / p.toReal) * ‖B‖ ^ (1 / p.toReal)) *54        (((2 : ℝ) ^ n)⁻¹) ^ (1 / p.toReal) := by55  have h := OperatorDomination.norm_maskedRestrictionLp_apply_le μ B G hG hdom56    p hp hptop M hM (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i)57    (norm_cellVector_le_one n i)58  apply h.trans59  calc60    _ ≤ M ^ (1 - 1 / p.toReal) * (‖B‖ * ((2 : ℝ) ^ n)⁻¹) ^ (1 / p.toReal) := by61      apply mul_le_mul_of_nonneg_left _ (Real.rpow_nonneg hM _)62      exact Real.rpow_le_rpow (norm_nonneg _)63        (norm_maskedRestriction_cell_le μ B G hG M n i hi) (by positivity)64    _ = _ := by rw [Real.mul_rpow (norm_nonneg B) (by positivity), mul_assoc]6566section Smoothing6768variable {Ω₂ H : Type*} [MeasurableSpace Ω₂] (ν : Measure Ω₂)69  [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]7071/-- Arbitrary operators before and after an Lp-to-Hilbert smoothing operator72have vanishing concrete interval dyadic traces. The extension identity is73required on the actual L1/Lp overlap; neither measure needs to be finite. -/74theorem trace_tendsto_zero_of_smoothing75    (A : Lp 𝕜 1 ν →L[𝕜] IntervalL1 𝕜) (S : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)76    (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)77    (p : ℝ≥0∞) (hp : 1 ≤ p) (hp2 : p < 2) [Fact (1 ≤ p)]78    (Q : Lp 𝕜 p μ →L[𝕜] H) (j : H →L[𝕜] Lp 𝕜 1 ν)79    (hS : ∀ (g : Lp 𝕜 1 μ) (f : Lp 𝕜 p μ), g =ᵐ[μ] f → S g = j (Q f)) :80    Tendsto (fun n => DyadicTrace.trace n (A.comp (S.comp B))) atTop (𝓝 0) := by81  have hptop : p ≠ ∞ := ne_top_of_lt hp282  have hpR : 1 ≤ p.toReal := by simpa using ENNReal.toReal_mono hptop hp83  have hp0 : 0 < p.toReal := lt_of_lt_of_le zero_lt_one hpR84  have hpR2 : p.toReal < 2 := by85    have h := (ENNReal.toReal_lt_toReal hptop (by norm_num : (2 : ℝ≥0∞) ≠ ∞)).mpr hp286    simpa using h87  have hr : (1 : ℝ) / 2 < 1 / p.toReal := (lt_div_iff₀ hp0).mpr (by linarith)88  obtain ⟨G, hG, hGint, hGpos, _, hdom⟩ := OperatorDomination.exists_measurable_dominator μ B89  let Bm (m : ℕ) : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ :=90    (L1Masks.mask μ {x | G x ≤ (m : ℝ)} (measurableSet_le hG measurable_const)).comp B91  let Rm (m : ℕ) : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜 := A.comp (S.comp (Bm m))92  have htrace (m : ℕ) : Tendsto (fun n => DyadicTrace.trace n (Rm m)) atTop (𝓝 0) := by93    let L := OperatorDomination.maskedRestrictionLp μ B G hG hdom p hp hptop94      (m : ℝ) (Nat.cast_nonneg m)95    have hfactor : DyadicTrace.restrictLinfty (Rm m) = (A.comp j).comp (Q.comp L) := by96      apply ContinuousLinearMap.ext97      intro f98      change A (S (OperatorDomination.maskedRestriction μ B G hG (m : ℝ) f)) = A (j (Q (L f)))99      rw [hS _ _ (OperatorDomination.coeFn_maskedRestrictionLp μ B G hG hdom100        p hp hptop (m : ℝ) (Nat.cast_nonneg m) f).symm]101    apply HilbertDyadicTrace.trace_tendsto_zero_of_power_bound (Rm m) (A.comp j) (Q.comp L)102      hfactor (‖Q‖ * ((m : ℝ) ^ (1 - 1 / p.toReal) * ‖B‖ ^ (1 / p.toReal)))103      (1 / p.toReal) (by positivity) hr104    intro n i hi105    change ‖Q (L (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i))‖ ≤ _106    have hcell : ‖L (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i)‖ ≤107        ((m : ℝ) ^ (1 - 1 / p.toReal) * ‖B‖ ^ (1 / p.toReal)) *108          (((2 : ℝ) ^ n)⁻¹) ^ (1 / p.toReal) :=109      norm_maskedRestrictionLp_cell_le (𝕜 := 𝕜) μ B G hG hdom p hp hptop110        (m : ℝ) (Nat.cast_nonneg m) n i hi111    exact (Q.le_opNorm (L (HilbertDyadicTrace.cellVector (𝕜 := 𝕜) n i))).trans112      ((mul_le_mul_of_nonneg_left hcell (norm_nonneg Q)).trans_eq (by ring))113  apply DyadicTrace.trace_tendsto_zero_of_approximation _ Rm htrace114  have heq (m : ℕ) : DyadicTrace.restrictLinfty (A.comp (S.comp B) - Rm m) =115      (A.comp S).comp (OperatorDomination.restriction μ (B - Bm m)) := by116    apply ContinuousLinearMap.ext117    intro f118    simp only [DyadicTrace.restrictLinfty, OperatorDomination.restriction,119      Rm, sub_apply, ContinuousLinearMap.comp_apply, map_sub]120  have hnorm (m : ℕ) : ‖DyadicTrace.restrictLinfty (A.comp (S.comp B) - Rm m)‖ ≤121      ‖A.comp S‖ * ‖OperatorDomination.restriction μ (B - Bm m)‖ := by122    rw [heq]123    exact ContinuousLinearMap.opNorm_comp_le _ _124  apply squeeze_zero (fun m => norm_nonneg _) hnorm125  simpa only [Bm, mul_zero] using126    (OperatorDomination.cutoff_approximation μ B G hG hGint hGpos hdom).const_mul ‖A.comp S‖127128theorem one_le_norm_id_sub_of_smoothing129    (A : Lp 𝕜 1 ν →L[𝕜] IntervalL1 𝕜) (S : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 ν)130    (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)131    (p : ℝ≥0∞) (hp : 1 ≤ p) (hp2 : p < 2) [Fact (1 ≤ p)]132    (Q : Lp 𝕜 p μ →L[𝕜] H) (j : H →L[𝕜] Lp 𝕜 1 ν)133    (hS : ∀ (g : Lp 𝕜 1 μ) (f : Lp 𝕜 p μ), g =ᵐ[μ] f → S g = j (Q f)) :134    1 ≤ ‖DyadicTrace.restrictLinfty135      (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) - A.comp (S.comp B))‖ :=136  DyadicTrace.one_le_norm_id_sub _ (trace_tendsto_zero_of_smoothing μ ν A S B p hp hp2 Q j hS)137138end Smoothing139140end PL1.SmoothingTrace141