PL1/EnfloTruncation.lean
All source files · Download exact source
SHA-256: 3e5c49af09fef9de86fa87a5a130664af58daa9c9dbb79142340291166d42fd6
1import PL1.EnfloMajorant2import PL1.LpInterpolation3import Mathlib.MeasureTheory.Integral.DominatedConvergence45/-! # Finite L1 family truncation under a common integrable majorant -/67noncomputable section8open MeasureTheory Filter9open scoped BigOperators Topology1011namespace PL1.EnfloBush1213def truncate (M z : ℝ) : ℝ := max (-M) (min M z)1415theorem truncate_eq_of_le (M z : ℝ) (hz : |z| ≤ M) : truncate M z = z := by16 obtain ⟨hl, hu⟩ := abs_le.mp hz17 rw [truncate, min_eq_right hu, max_eq_right hl]1819theorem abs_truncate_le (M z : ℝ) (hM : 0 ≤ M) : |truncate M z| ≤ M := by20 apply abs_le.mpr21 exact ⟨le_max_left _ _, max_le (by linarith) (min_le_left _ _)⟩2223theorem abs_sub_truncate (M z : ℝ) (hM : 0 ≤ M) :24 |z - truncate M z| = max (|z| - M) 0 := by25 by_cases hp : M < z26 · have hz : 0 ≤ z := hM.trans hp.le27 rw [truncate, min_eq_left hp.le, max_eq_right (by linarith : -M ≤ M),28 abs_of_nonneg (sub_nonneg.mpr hp.le), abs_of_nonneg hz,29 max_eq_left (sub_nonneg.mpr hp.le)]30 · by_cases hn : z < -M31 · have hz : z ≤ 0 := hn.le.trans (by linarith)32 rw [truncate, min_eq_right (by linarith : z ≤ M), max_eq_left hn.le,33 abs_of_nonpos (by linarith : z - -M ≤ 0), abs_of_nonpos hz,34 max_eq_left (by linarith : 0 ≤ -z - M)]35 ring36 · have hz : |z| ≤ M := abs_le.mpr ⟨le_of_not_gt hn, le_of_not_gt hp⟩37 rw [truncate_eq_of_le M z hz, sub_self, abs_zero, max_eq_right (sub_nonpos.mpr hz)]3839theorem abs_truncate_le_abs (M z : ℝ) (hM : 0 ≤ M) : |truncate M z| ≤ |z| := by40 by_cases hz : |z| ≤ M41 · rw [truncate_eq_of_le M z hz]42 · exact (abs_truncate_le M z hM).trans (le_of_lt (lt_of_not_ge hz))4344theorem abs_sub_truncate_le (M z : ℝ) (hM : 0 ≤ M) : |z - truncate M z| ≤ |z| := by45 rw [abs_sub_truncate M z hM]46 exact max_le (by linarith) (abs_nonneg _)4748theorem tail_add_le {M a b : ℝ} (hM : 0 ≤ M) (ha : 0 ≤ a) (hb : 0 ≤ b) :49 max (a - M) 0 + max (b - M) 0 ≤ max (a + b - M) 0 := by50 by_cases haM : a ≤ M <;> by_cases hbM : b ≤ M51 · rw [max_eq_right (sub_nonpos.mpr haM), max_eq_right (sub_nonpos.mpr hbM)]52 simpa only [zero_add] using le_max_right (a + b - M) 053 · rw [max_eq_right (sub_nonpos.mpr haM), max_eq_left (by linarith : 0 ≤ b - M), zero_add]54 exact (by linarith : b - M ≤ a + b - M).trans (le_max_left _ _)55 · rw [max_eq_left (by linarith : 0 ≤ a - M), max_eq_right (sub_nonpos.mpr hbM), add_zero]56 exact (by linarith : a - M ≤ a + b - M).trans (le_max_left _ _)57 · rw [max_eq_left (by linarith : 0 ≤ a - M), max_eq_left (by linarith : 0 ≤ b - M)]58 exact (by linarith : a - M + (b - M) ≤ a + b - M).trans (le_max_left _ _)5960theorem sum_truncation_error_le (n : ℕ) (a : ℕ → ℝ) {M : ℝ} (hM : 0 ≤ M) :61 (∑ j ∈ Finset.range n, |a j - truncate M (a j)|) ≤62 max ((∑ j ∈ Finset.range n, |a j|) - M) 0 := by63 induction n with64 | zero => simp65 | succ n ih =>66 rw [Finset.sum_range_succ, Finset.sum_range_succ, abs_sub_truncate M (a n) hM]67 exact (add_le_add ih le_rfl).trans68 (tail_add_le hM (Finset.sum_nonneg (fun _ _ => abs_nonneg _)) (abs_nonneg _))6970section L171variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}7273theorem integrable_truncate (M : ℝ) (hM : 0 ≤ M) (f : Lp ℝ 1 μ) :74 Integrable (fun x => truncate M (f x)) μ := by75 apply (L1.integrable_coeFn f).mono76 · exact aestronglyMeasurable_const.sup (aestronglyMeasurable_const.inf (Lp.aestronglyMeasurable f))77 · exact Filter.Eventually.of_forall (fun x => by78 simpa only [Real.norm_eq_abs] using abs_truncate_le_abs M (f x) hM)7980def truncateLp (M : ℝ) (hM : 0 ≤ M) (f : Lp ℝ 1 μ) : Lp ℝ 1 μ :=81 (integrable_truncate M hM f).toL1 (fun x => truncate M (f x))8283theorem truncateLp_coe (M : ℝ) (hM : 0 ≤ M) (f : Lp ℝ 1 μ) :84 truncateLp M hM f =ᵐ[μ] (fun x => truncate M (f x)) :=85 (integrable_truncate M hM f).coeFn_toL18687theorem truncateLp_bound (M : ℝ) (hM : 0 ≤ M) (f : Lp ℝ 1 μ) :88 ∀ᵐ x ∂μ, ‖truncateLp M hM f x‖ ≤ M := by89 filter_upwards [truncateLp_coe M hM f] with x hx90 rw [hx, Real.norm_eq_abs]91 exact abs_truncate_le M (f x) hM9293theorem norm_truncateLp_le (M : ℝ) (hM : 0 ≤ M) (f : Lp ℝ 1 μ) :94 ‖truncateLp M hM f‖ ≤ ‖f‖ := by95 rw [L1.norm_eq_integral_norm, L1.norm_eq_integral_norm]96 apply integral_mono_ae (L1.integrable_coeFn _).norm (L1.integrable_coeFn _).norm97 filter_upwards [truncateLp_coe M hM f] with x hx98 rw [hx, Real.norm_eq_abs, Real.norm_eq_abs]99 exact abs_truncate_le_abs M (f x) hM100101theorem sum_norm_truncation_error_le (n : ℕ) (f : ℕ → Lp ℝ 1 μ)102 (M : ℝ) (hM : 0 ≤ M) (g : Ω → ℝ) (hg : Integrable g μ) (hg0 : ∀ x, 0 ≤ g x)103 (hfg : ∀ᵐ x ∂μ, (∑ j ∈ Finset.range n, |f j x|) ≤ g x) :104 (∑ j ∈ Finset.range n, ‖f j - truncateLp M hM (f j)‖) ≤105 ∫ x, max (g x - M) 0 ∂μ := by106 have hgI : Integrable (fun x => max (g x - M) 0) μ := by107 apply hg.mono'108 · exact (hg.aestronglyMeasurable.sub aestronglyMeasurable_const).sup aestronglyMeasurable_const109 · exact Filter.Eventually.of_forall (fun x => by110 rw [Real.norm_eq_abs, abs_of_nonneg (le_max_right _ _)]111 exact max_le (by linarith) (hg0 x))112 have he (j : ℕ) : ‖f j - truncateLp M hM (f j)‖ = ∫ x, |f j x - truncate M (f j x)| ∂μ := by113 rw [L1.norm_eq_integral_norm]114 apply integral_congr_ae115 filter_upwards [Lp.coeFn_sub (f j) (truncateLp M hM (f j)), truncateLp_coe M hM (f j)] with x hx ht116 rw [hx, Pi.sub_apply, ht, Real.norm_eq_abs]117 simp_rw [he]118 have herr (j : ℕ) : Integrable (fun x => |f j x - truncate M (f j x)|) μ := by119 simpa only [Pi.sub_apply] using ((L1.integrable_coeFn (f j)).sub120 (integrable_truncate M hM (f j))).abs121 rw [← integral_finsetSum _ (fun j _ => herr j)]122 apply integral_mono_ae (integrable_finsetSum _ (fun j _ => herr j)) hgI123 filter_upwards [hfg] with x hx124 exact (sum_truncation_error_le n (fun j => f j x) hM).trans (max_le_max (sub_le_sub_right hx M) le_rfl)125126theorem integral_tail_tendsto_zero (g : Ω → ℝ) (hg : Integrable g μ) (hg0 : ∀ x, 0 ≤ g x) :127 Tendsto (fun n : ℕ => ∫ x, max (g x - (n : ℝ)) 0 ∂μ) atTop (𝓝 0) := by128 have h := tendsto_integral_of_dominated_convergence g129 (fun n => (hg.aestronglyMeasurable.sub aestronglyMeasurable_const).sup aestronglyMeasurable_const)130 hg (fun n => Filter.Eventually.of_forall (fun x => by131 rw [Real.norm_eq_abs, abs_of_nonneg (le_max_right _ _)]132 exact max_le (sub_le_self _ (Nat.cast_nonneg n)) (hg0 x)))133 (Filter.Eventually.of_forall (fun x => by134 apply tendsto_const_nhds.congr'135 obtain ⟨N, hN⟩ := exists_nat_ge (g x)136 filter_upwards [eventually_ge_atTop N] with n hn137 have he : g x ≤ (n : ℝ) := hN.trans (by exact_mod_cast hn)138 exact (max_eq_right (sub_nonpos.mpr he)).symm))139 simpa only [integral_zero, Pi.sup_apply, Pi.sub_apply] using h140141end L1142143#print axioms sum_norm_truncation_error_le144#print axioms integral_tail_tendsto_zero145end PL1.EnfloBush146