PL1/OperatorDomination.lean
All source files · Download exact source
SHA-256: 23aca0a207116e49375e60a1b4d5abb47287ca9ee80e68dcfa80a9128e0dc53b
1import PL1.IntervalDyadicApproximation2import Mathlib.MeasureTheory.Integral.DominatedConvergence34/-! # Domination and target truncation for operators out of interval L1 -/56noncomputable section7set_option autoImplicit false8set_option maxHeartbeats 8000009open MeasureTheory Filter10open scoped ENNReal Topology1112namespace PL1.OperatorDomination1314attribute [local instance] DyadicTrace.intervalMeasure_probability1516variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω] (μ : Measure Ω)1718def restriction (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ) :19 Lp 𝕜 ∞ intervalMeasure →L[𝕜] Lp 𝕜 1 μ :=20 B.comp (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top)2122theorem exists_measurable_dominator (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ) :23 ∃ G : Ω → ℝ, Measurable G ∧ Integrable G μ ∧ (∀ x, 0 ≤ G x) ∧24 (∫ x, G x ∂μ) ≤ ‖B‖ ∧ ∀ f : Lp 𝕜 ∞ intervalMeasure, ‖f‖ ≤ 1 →25 ∀ᵐ x ∂μ, ‖restriction μ B f x‖ ≤ G x := by26 obtain ⟨g, hg, hgpos, hgint, hgdom⟩ := DyadicTrace.exists_integrable_dominator μ B27 let G : Ω → ℝ := fun x => max 0 (hg.aestronglyMeasurable.mk g x)28 have hGmeas : Measurable G := measurable_const.max hg.aestronglyMeasurable.measurable_mk29 have hGae : g =ᵐ[μ] G := by30 filter_upwards [hg.aestronglyMeasurable.ae_eq_mk] with x hx31 change g x = max 0 (hg.aestronglyMeasurable.mk g x)32 rw [← hx, max_eq_right (hgpos x)]33 refine ⟨G, hGmeas, hg.congr hGae, fun x => le_max_left _ _, ?_, ?_⟩34 · rw [← integral_congr_ae hGae]35 exact hgint36 · intro f hf37 filter_upwards [hgdom f hf, hGae] with x hx hxx38 exact hx.trans_eq hxx3940theorem norm_mask_restriction_le (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)41 (G : Ω → ℝ) (hG : Integrable G μ) (hGpos : ∀ x, 0 ≤ G x)42 (hdom : ∀ f : Lp 𝕜 ∞ intervalMeasure, ‖f‖ ≤ 1 →43 ∀ᵐ x ∂μ, ‖restriction μ B f x‖ ≤ G x)44 (A : Set Ω) (hA : MeasurableSet A) :45 ‖(L1Masks.mask μ A hA).comp (restriction μ B)‖ ≤ ∫ x in A, G x ∂μ := by46 apply ContinuousLinearMap.opNorm_le_of_unit_norm (integral_nonneg hGpos)47 intro f hf48 change ‖L1Masks.mask μ A hA (restriction μ B f)‖ ≤ _49 rw [L1Masks.norm_mask]50 exact integral_mono_ae (L1.integrable_coeFn (restriction μ B f)).norm.integrableOn51 hG.integrableOn (ae_restrict_of_ae (hdom f hf.le))5253theorem mask_compl (A : Set Ω) (hA : MeasurableSet A) :54 ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 μ) - L1Masks.mask μ A hA =55 L1Masks.mask μ Aᶜ hA.compl := by56 apply ContinuousLinearMap.ext57 intro f58 apply Lp.ext59 change (f - L1Masks.mask μ A hA f : Lp 𝕜 1 μ) =ᵐ[μ] L1Masks.mask μ Aᶜ hA.compl f60 filter_upwards [Lp.coeFn_sub f (L1Masks.mask μ A hA f),61 L1Masks.coeFn_mask μ A hA f, L1Masks.coeFn_mask μ Aᶜ hA.compl f] with x hs ha hc62 rw [hs, Pi.sub_apply, ha, hc]63 by_cases hx : x ∈ A <;> simp [hx]6465theorem integral_upper_tail_tendsto_zero (G : Ω → ℝ)66 (hGmeas : Measurable G) (hG : Integrable G μ) (hGpos : ∀ x, 0 ≤ G x) :67 Tendsto (fun n : ℕ => ∫ x in {x | (n : ℝ) < G x}, G x ∂μ) atTop (𝓝 0) := by68 have hm (n : ℕ) : MeasurableSet {x | (n : ℝ) < G x} := measurableSet_lt measurable_const hGmeas69 have ht := tendsto_integral_of_dominated_convergence (μ := μ) (f := fun _ => (0 : ℝ)) G70 (fun n => (hGmeas.indicator (hm n)).aestronglyMeasurable) hG71 (fun n => ae_of_all _ (fun x => by72 by_cases hx : (n : ℝ) < G x73 · rw [Set.indicator_of_mem (show x ∈ {x | (n : ℝ) < G x} from hx)]74 simp only [Real.norm_eq_abs, abs_of_nonneg (hGpos x), le_refl]75 · rw [Set.indicator_of_notMem (show x ∉ {x | (n : ℝ) < G x} from hx), norm_zero]76 exact hGpos x))77 (ae_of_all _ (fun x => by78 obtain ⟨N, hN⟩ := exists_nat_gt (G x)79 apply tendsto_const_nhds.congr'80 filter_upwards [eventually_ge_atTop N] with n hn81 have hle : G x ≤ (n : ℝ) := hN.le.trans (by exact_mod_cast hn)82 exact (Set.indicator_of_notMem83 (show x ∉ {x | (n : ℝ) < G x} from not_lt.mpr hle) G).symm))84 simpa only [integral_indicator (hm _), integral_zero] using ht8586theorem norm_cutoff_error_le (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)87 (G : Ω → ℝ) (hGmeas : Measurable G) (hG : Integrable G μ) (hGpos : ∀ x, 0 ≤ G x)88 (hdom : ∀ f : Lp 𝕜 ∞ intervalMeasure, ‖f‖ ≤ 1 →89 ∀ᵐ x ∂μ, ‖restriction μ B f x‖ ≤ G x) (M : ℝ) :90 ‖restriction μ (B - (L1Masks.mask μ {x | G x ≤ M}91 (measurableSet_le hGmeas measurable_const)).comp B)‖ ≤92 ∫ x in {x | M < G x}, G x ∂μ := by93 have hset : {x | G x ≤ M}ᶜ = {x | M < G x} := by ext x; simp94 have heq : B - (L1Masks.mask μ {x | G x ≤ M}95 (measurableSet_le hGmeas measurable_const)).comp B =96 (L1Masks.mask μ {x | M < G x} (measurableSet_lt measurable_const hGmeas)).comp B := by97 calc98 _ = (ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 μ) - L1Masks.mask μ {x | G x ≤ M}99 (measurableSet_le hGmeas measurable_const)).comp B := by100 rw [ContinuousLinearMap.sub_comp, ContinuousLinearMap.id_comp]101 _ = _ := by rw [mask_compl]; simp only [hset]102 rw [heq]103 simpa only [restriction, ContinuousLinearMap.comp_assoc] using104 norm_mask_restriction_le μ B G hG hGpos hdom {x | M < G x}105 (measurableSet_lt measurable_const hGmeas)106107theorem cutoff_approximation (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)108 (G : Ω → ℝ) (hGmeas : Measurable G) (hG : Integrable G μ) (hGpos : ∀ x, 0 ≤ G x)109 (hdom : ∀ f : Lp 𝕜 ∞ intervalMeasure, ‖f‖ ≤ 1 →110 ∀ᵐ x ∂μ, ‖restriction μ B f x‖ ≤ G x) :111 Tendsto (fun n : ℕ => ‖restriction μ (B - (L1Masks.mask μ {x | G x ≤ (n : ℝ)}112 (measurableSet_le hGmeas measurable_const)).comp B)‖) atTop (𝓝 0) := by113 exact squeeze_zero (fun n => norm_nonneg _) (fun n =>114 norm_cutoff_error_le μ B G hGmeas hG hGpos hdom n)115 (integral_upper_tail_tendsto_zero μ G hGmeas hG hGpos)116117end PL1.OperatorDomination118