PL1/TraceDomination.lean
All source files · Download exact source
SHA-256: e9aef601268b8155274cbd1dfd77a518c1c38c79ab595a3d9aebbf300626814f
1import PL1.DyadicTrace2import Mathlib.MeasureTheory.Function.ConvergenceInMeasure34/-! # Integrable envelopes and domination under L1 approximation56The target measure is arbitrary; in particular it may have infinite mass.7-/89noncomputable section10set_option autoImplicit false11set_option maxHeartbeats 80000012open MeasureTheory Filter13open scoped ENNReal BigOperators Topology1415namespace PL1.TraceDomination1617variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)1819/-- A monotone sequence of nonnegative integrable functions whose integrals20are uniformly bounded has an integrable common upper bound. -/21theorem exists_integrable_envelope (g : ℕ → Ω → ℝ)22 (hg : ∀ n, Integrable (g n) μ) (hpos : ∀ n x, 0 ≤ g n x)23 (hmono : ∀ᵐ x ∂μ, Monotone (fun n => g n x))24 (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ n, ∫ x, g n x ∂μ ≤ C) :25 ∃ G : Ω → ℝ, Integrable G μ ∧ (∀ x, 0 ≤ G x) ∧26 (∫ x, G x ∂μ) ≤ C ∧ ∀ n, g n ≤ᵐ[μ] G := by27 let genv : Ω → ℝ≥0∞ := fun x => ⨆ n, ENNReal.ofReal (g n x)28 have hgmeas (n : ℕ) : AEMeasurable (fun x => ENNReal.ofReal (g n x)) μ :=29 (hg n).aemeasurable.ennreal_ofReal30 have hGmeas : AEMeasurable genv μ := .iSup hgmeas31 have hGeq : (∫⁻ x, genv x ∂μ) = ⨆ n, ∫⁻ x, ENNReal.ofReal (g n x) ∂μ := by32 apply lintegral_iSup' hgmeas33 exact hmono.mono (fun x hx n m hnm => ENNReal.ofReal_le_ofReal (hx hnm))34 have hGbound : (∫⁻ x, genv x ∂μ) ≤ ENNReal.ofReal C := by35 rw [hGeq]36 apply iSup_le37 intro n38 rw [← ofReal_integral_eq_lintegral_ofReal (hg n) (ae_of_all _ (hpos n))]39 exact ENNReal.ofReal_le_ofReal (hbound n)40 have hGfinite : (∫⁻ x, genv x ∂μ) ≠ ∞ := ne_top_of_le_ne_top ENNReal.ofReal_ne_top hGbound41 have hGae : ∀ᵐ x ∂μ, genv x < ∞ := ae_lt_top' hGmeas hGfinite42 refine ⟨fun x => (genv x).toReal, integrable_toReal_of_lintegral_ne_top hGmeas hGfinite,43 fun x => ENNReal.toReal_nonneg, ?_, ?_⟩44 · rw [integral_toReal hGmeas hGae]45 have h := ENNReal.toReal_mono ENNReal.ofReal_ne_top hGbound46 simpa only [ENNReal.toReal_ofReal hC] using h47 · intro n48 filter_upwards [hGae] with x hx49 have h := ENNReal.toReal_mono hx.ne (le_iSup (fun m => ENNReal.ofReal (g m x)) n)50 simpa only [ENNReal.toReal_ofReal (hpos n x)] using h5152/-- A common almost-everywhere norm bound passes through convergence in L1. -/53theorem ae_norm_le_of_tendsto_L1 {𝕜 : Type*} [RCLike 𝕜]54 (f : ℕ → Lp 𝕜 1 μ) (g : Lp 𝕜 1 μ) (G : Ω → ℝ)55 (hf : Tendsto f atTop (𝓝 g)) (hbound : ∀ n, ∀ᵐ x ∂μ, ‖f n x‖ ≤ G x) :56 ∀ᵐ x ∂μ, ‖g x‖ ≤ G x := by57 obtain ⟨φ, hφ, ht⟩ := (tendstoInMeasure_of_tendsto_Lp hf).exists_seq_tendsto_ae58 filter_upwards [ht, ae_all_iff.2 hbound] with x hx hb59 exact le_of_tendsto hx.norm (Eventually.of_forall (fun n => hb (φ n)))6061private theorem sum_pairs (f : ℕ → ℝ) (N : ℕ) :62 (∑ k ∈ Finset.range (2 * N), f k) =63 ∑ i ∈ Finset.range N, (f (2 * i) + f (2 * i + 1)) := by64 induction N with65 | zero => simp66 | succ N ih =>67 rw [Nat.mul_succ]68 simp only [show 2 * N + 2 = (2 * N + 1) + 1 by omega,69 Finset.sum_range_succ, ih]70 ring7172section BinaryApproximation7374variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]75variable (e : ℕ → ℕ → E) (B : E →L[𝕜] Lp 𝕜 1 μ)7677def binaryEnvelope (n : ℕ) (x : Ω) : ℝ :=78 ∑ i ∈ Finset.range (2 ^ n), ‖B (e n i) x‖7980theorem binaryEnvelope_nonneg (n : ℕ) (x : Ω) : 0 ≤ binaryEnvelope μ e B n x :=81 Finset.sum_nonneg (fun _i _ => norm_nonneg _)8283theorem integrable_binaryEnvelope (n : ℕ) : Integrable (binaryEnvelope μ e B n) μ :=84 integrable_finsetSum _ (fun i _ => (L1.integrable_coeFn (B (e n i))).norm)8586theorem integral_binaryEnvelope_le (hmass : ∀ n, ∑ i ∈ Finset.range (2 ^ n), ‖e n i‖ ≤ 1)87 (n : ℕ) : (∫ x, binaryEnvelope μ e B n x ∂μ) ≤ ‖B‖ := by88 unfold binaryEnvelope89 rw [integral_finsetSum _ (fun i _ => (L1.integrable_coeFn (B (e n i))).norm)]90 simp only [← L1.norm_eq_integral_norm]91 calc92 _ ≤ ∑ i ∈ Finset.range (2 ^ n), ‖B‖ * ‖e n i‖ := Finset.sum_le_sum (fun i _ => B.le_opNorm _)93 _ = ‖B‖ * ∑ i ∈ Finset.range (2 ^ n), ‖e n i‖ := by rw [Finset.mul_sum]94 _ ≤ ‖B‖ * 1 := mul_le_mul_of_nonneg_left (hmass n) (norm_nonneg _)95 _ = ‖B‖ := mul_one _9697theorem binaryEnvelope_monotone98 (hrefine : ∀ n i, i < 2 ^ n → e n i = e (n + 1) (2 * i) + e (n + 1) (2 * i + 1)) :99 ∀ᵐ x ∂μ, Monotone (fun n => binaryEnvelope μ e B n x) := by100 have href (n i : ℕ) : ∀ᵐ x ∂μ, i < 2 ^ n →101 B (e n i) x = B (e (n + 1) (2 * i)) x + B (e (n + 1) (2 * i + 1)) x := by102 by_cases hi : i < 2 ^ n103 · rw [hrefine n i hi, map_add]104 filter_upwards [Lp.coeFn_add (B (e (n + 1) (2 * i)))105 (B (e (n + 1) (2 * i + 1)))] with x hx106 exact fun _ => hx107 · exact ae_of_all _ (fun _ h => (hi h).elim)108 filter_upwards [ae_all_iff.2 (fun n => ae_all_iff.2 (href n))] with x hx109 apply monotone_nat_of_le_succ110 intro n111 unfold binaryEnvelope112 rw [pow_succ, Nat.mul_comm (2 ^ n) 2, sum_pairs]113 apply Finset.sum_le_sum114 intro i hi115 rw [hx n i (Finset.mem_range.mp hi)]116 exact norm_add_le _ _117118theorem ae_norm_linearCombination_le_binaryEnvelope (n : ℕ) (c : ℕ → 𝕜)119 (hc : ∀ i, ‖c i‖ ≤ 1) :120 ∀ᵐ x ∂μ, ‖B (∑ i ∈ Finset.range (2 ^ n), c i • e n i) x‖ ≤ binaryEnvelope μ e B n x := by121 simp only [map_sum, map_smul]122 filter_upwards [Lp.coeFn_fun_finsetSum (Finset.range (2 ^ n))123 (fun i => c i • B (e n i)), ae_all_iff.2 (fun i => Lp.coeFn_smul (c i) (B (e n i)))]124 with x hsum hsmul125 rw [hsum]126 calc127 _ ≤ ∑ i ∈ Finset.range (2 ^ n), ‖(c i • B (e n i)) x‖ := norm_sum_le _ _128 _ ≤ binaryEnvelope μ e B n x := by129 apply Finset.sum_le_sum130 intro i hi131 rw [hsmul i]132 change ‖c i • B (e n i) x‖ ≤ _133 rw [norm_smul]134 exact (mul_le_mul_of_nonneg_right (hc i) (norm_nonneg _)).trans_eq (one_mul _)135136/-- An operator on a source with binary bounded step approximations admits137one integrable envelope for the specified bounded subset. No finiteness138assumption is imposed on the target measure. -/139theorem exists_dominator_of_binary_approximation140 (hrefine : ∀ n i, i < 2 ^ n → e n i = e (n + 1) (2 * i) + e (n + 1) (2 * i + 1))141 (hmass : ∀ n, ∑ i ∈ Finset.range (2 ^ n), ‖e n i‖ ≤ 1)142 (U : Set E)143 (happrox : ∀ f ∈ U, ∃ c : ℕ → ℕ → 𝕜,144 (∀ n i, ‖c n i‖ ≤ 1) ∧ Tendsto145 (fun n => ∑ i ∈ Finset.range (2 ^ n), c n i • e n i) atTop (𝓝 f)) :146 ∃ G : Ω → ℝ, Integrable G μ ∧ (∀ x, 0 ≤ G x) ∧147 (∫ x, G x ∂μ) ≤ ‖B‖ ∧ ∀ f ∈ U, ∀ᵐ x ∂μ, ‖B f x‖ ≤ G x := by148 obtain ⟨G, hG, hGpos, hGint, hGbound⟩ := exists_integrable_envelope μ149 (binaryEnvelope μ e B) (integrable_binaryEnvelope μ e B) (binaryEnvelope_nonneg μ e B)150 (binaryEnvelope_monotone μ e B hrefine) ‖B‖ (norm_nonneg _)151 (integral_binaryEnvelope_le μ e B hmass)152 refine ⟨G, hG, hGpos, hGint, ?_⟩153 intro f hf154 obtain ⟨c, hc, hcf⟩ := happrox f hf155 apply ae_norm_le_of_tendsto_L1 μ156 (fun n => B (∑ i ∈ Finset.range (2 ^ n), c n i • e n i))157 (B f) G (B.continuous.tendsto f |>.comp hcf)158 intro n159 filter_upwards [ae_norm_linearCombination_le_binaryEnvelope μ e B n (c n) (hc n),160 hGbound n] with x hx hy161 exact hx.trans hy162163end BinaryApproximation164165end PL1.TraceDomination166167