PL1/DyadicInterpolationIntegral.lean
All source files · Download exact source
SHA-256: 0e9e77401af852bbd4166ebeb72ca017310a979b44a314bbf6711198ddf860ff
1import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals2import Mathlib.MeasureTheory.Integral.Lebesgue.Countable3import Mathlib.Tactic.Positivity4import Mathlib.Tactic.Linarith5import Mathlib.Tactic.NormNum6import Mathlib.Tactic.Ring78/-! # Dyadic sampling of the continuous real interpolation integral910All integrals and series take values in ENNReal, so the comparisons include11infinite norms and imply equivalence of the corresponding membership tests.12-/1314noncomputable section15open MeasureTheory Filter Set16open scoped ENNReal Topology1718namespace PL1.DyadicInterpolation1920def time (n : ℕ) : ℝ := (1 / 2 : ℝ) ^ n21def shell (n : ℕ) : Set ℝ := Ioc (time (n + 1)) (time n)22def weight (n : ℕ) : ℝ := (time n) ^ (-1 / 2 : ℝ)23def sample (k : ℝ → ℝ) (n : ℕ) : ℝ≥0∞ := ENNReal.ofReal (weight n * k (time n))24def integrand (k : ℝ → ℝ) (t : ℝ) : ℝ≥0∞ := ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * k t)25def smallIntegral (k : ℝ → ℝ) : ℝ≥0∞ := ∫⁻ t in Ioc (0 : ℝ) 1, integrand k t26def fullIntegral (k : ℝ → ℝ) : ℝ≥0∞ := ∫⁻ t in Ioi (0 : ℝ), integrand k t27def lowerConstant : ℝ := (1 / 2 : ℝ) ^ (1 / 2 : ℝ) / 228def upperConstant : ℝ := (1 / 2 : ℝ) ^ (-3 / 2 : ℝ) / 22930@[simp] theorem time_zero : time 0 = 1 := by simp [time]31theorem time_pos (n : ℕ) : 0 < time n := by unfold time; positivity32theorem time_succ (n : ℕ) : time (n + 1) = time n / 2 := by simp [time, pow_succ, div_eq_mul_inv]33theorem time_antitone : Antitone time := fun _ _ h => pow_le_pow_of_le_one (by norm_num) (by norm_num) h34theorem time_le_one (n : ℕ) : time n ≤ 1 := by simpa using time_antitone (Nat.zero_le n)35theorem tendsto_time : Tendsto time atTop (𝓝 0) :=36 tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num)37theorem weight_pos (n : ℕ) : 0 < weight n := Real.rpow_pos_of_pos (time_pos n) _38theorem lowerConstant_pos : 0 < lowerConstant := by unfold lowerConstant; positivity39theorem upperConstant_pos : 0 < upperConstant := by unfold upperConstant; positivity4041theorem shells_disjoint : Pairwise (fun m n => Disjoint (shell m) (shell n)) := by42 have aux (m n : ℕ) (hlt : m < n) : Disjoint (shell m) (shell n) := by43 apply Set.disjoint_left.mpr44 intro x hx hy45 have h := time_antitone (Nat.succ_le_of_lt hlt)46 exact (not_lt_of_ge (hy.2.trans h)) hx.147 intro m n hmn48 obtain h | h := lt_or_gt_of_ne hmn49 · exact aux m n h50 · exact (aux n m h).symm5152theorem union_shells : (⋃ n, shell n) = Ioc (0 : ℝ) 1 := by53 ext t54 constructor55 · intro ht56 obtain ⟨n, hn⟩ := Set.mem_iUnion.mp ht57 exact ⟨(time_pos (n + 1)).trans hn.1, hn.2.trans (time_le_one n)⟩58 · intro ht59 have hex : ∃ n, time n < t :=60 (tendsto_time.eventually (gt_mem_nhds ht.1)).exists61 have hfind := Nat.find_spec hex62 have hn0 : Nat.find hex ≠ 0 := by intro he; rw [he, time_zero] at hfind; linarith [ht.2]63 obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero hn064 apply Set.mem_iUnion.mpr65 refine ⟨n, ?_⟩66 change time (n + 1) < t ∧ t ≤ time n67 constructor68 · simpa only [hn] using hfind69 · exact not_lt.mp (Nat.find_min hex (by omega))7071theorem smallIntegral_eq_tsum (k : ℝ → ℝ) :72 smallIntegral k = ∑' n, ∫⁻ t in shell n, integrand k t := by73 rw [smallIntegral, ← union_shells]74 exact lintegral_iUnion (fun _ => measurableSet_Ioc) shells_disjoint _7576theorem volume_shell (n : ℕ) : volume (shell n) = ENNReal.ofReal (time n / 2) := by77 rw [shell, Real.volume_Ioc, time_succ]78 congr 179 ring8081theorem rpow_length (n : ℕ) :82 (time n) ^ (-3 / 2 : ℝ) * (time n / 2) = weight n / 2 := by83 unfold weight84 rw [← mul_div_assoc]85 congr 186 calc87 _ = (time n) ^ (-3 / 2 : ℝ) * (time n) ^ (1 : ℝ) := by rw [Real.rpow_one]88 _ = _ := by rw [← Real.rpow_add (time_pos n)]; norm_num8990theorem weight_succ (n : ℕ) :91 weight (n + 1) = weight n * (1 / 2 : ℝ) ^ (-1 / 2 : ℝ) := by92 unfold weight time93 rw [pow_succ, Real.mul_rpow (by positivity) (by norm_num)]9495theorem lower_length (n : ℕ) :96 lowerConstant * weight (n + 1) = (time n) ^ (-3 / 2 : ℝ) * (time n / 2) := by97 rw [rpow_length, weight_succ]98 have hh : (1 / 2 : ℝ) ^ (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ (-1 / 2 : ℝ) = 1 := by99 rw [← Real.rpow_add (by norm_num : (0 : ℝ) < 1 / 2)]100 norm_num101 unfold lowerConstant102 nlinarith [congrArg (fun z : ℝ => z * weight n) hh]103104theorem upper_length (n : ℕ) :105 (time (n + 1)) ^ (-3 / 2 : ℝ) * (time n / 2) = upperConstant * weight n := by106 have ht : time (n + 1) = time n * (1 / 2) := by rw [time_succ]; ring107 rw [ht, Real.mul_rpow (time_pos n).le (by norm_num)]108 have hr := rpow_length n109 unfold upperConstant110 nlinarith [congrArg (fun z : ℝ => z * (1 / 2 : ℝ) ^ (-3 / 2 : ℝ)) hr]111112variable {k : ℝ → ℝ}113114theorem shell_bounds (hk : ∀ t ∈ Ici (0 : ℝ), 0 ≤ k t)115 (hmono : MonotoneOn k (Ici (0 : ℝ))) (n : ℕ) :116 ENNReal.ofReal lowerConstant * sample k (n + 1) ≤ ∫⁻ t in shell n, integrand k t ∧117 (∫⁻ t in shell n, integrand k t) ≤ ENNReal.ofReal upperConstant * sample k n := by118 have hlo (t : ℝ) (ht : t ∈ shell n) :119 (time n) ^ (-3 / 2 : ℝ) * k (time (n + 1)) ≤ t ^ (-3 / 2 : ℝ) * k t := by120 have ht0 : 0 < t := (time_pos (n + 1)).trans ht.1121 exact mul_le_mul (Real.rpow_le_rpow_of_nonpos ht0 ht.2 (by norm_num))122 (hmono (time_pos _).le ht0.le ht.1.le) (hk _ (time_pos _).le)123 (Real.rpow_nonneg ht0.le _)124 have hhi (t : ℝ) (ht : t ∈ shell n) :125 t ^ (-3 / 2 : ℝ) * k t ≤ (time (n + 1)) ^ (-3 / 2 : ℝ) * k (time n) := by126 have ht0 : 0 < t := (time_pos (n + 1)).trans ht.1127 exact mul_le_mul (Real.rpow_le_rpow_of_nonpos (time_pos _) ht.1.le (by norm_num))128 (hmono ht0.le (time_pos _).le ht.2) (hk _ ht0.le)129 (Real.rpow_nonneg (time_pos _).le _)130 have h1 : ENNReal.ofReal ((time n) ^ (-3 / 2 : ℝ) * k (time (n + 1))) * volume (shell n) ≤131 ∫⁻ t in shell n, integrand k t := by132 rw [← setLIntegral_const]133 exact setLIntegral_mono' measurableSet_Ioc (fun t ht => ENNReal.ofReal_le_ofReal (hlo t ht))134 have h2 : (∫⁻ t in shell n, integrand k t) ≤135 ENNReal.ofReal ((time (n + 1)) ^ (-3 / 2 : ℝ) * k (time n)) * volume (shell n) := by136 rw [← setLIntegral_const]137 exact setLIntegral_mono' measurableSet_Ioc (fun t ht => ENNReal.ofReal_le_ofReal (hhi t ht))138 rw [volume_shell, ← ENNReal.ofReal_mul139 (mul_nonneg (Real.rpow_nonneg (time_pos n).le _) (hk _ (time_pos (n + 1)).le))] at h1140 rw [volume_shell, ← ENNReal.ofReal_mul141 (mul_nonneg (Real.rpow_nonneg (time_pos (n + 1)).le _) (hk _ (time_pos n).le))] at h2142 constructor143 · convert h1 using 1144 rw [sample, ← ENNReal.ofReal_mul lowerConstant_pos.le]145 congr 1146 calc147 _ = (lowerConstant * weight (n + 1)) * k (time (n + 1)) := by ring148 _ = _ := by rw [lower_length]; ring149 · convert h2 using 1150 rw [sample, ← ENNReal.ofReal_mul upperConstant_pos.le]151 congr 1152 calc153 _ = (upperConstant * weight n) * k (time n) := by ring154 _ = _ := by rw [← upper_length]; ring155156theorem smallIntegral_bounds (hk : ∀ t ∈ Ici (0 : ℝ), 0 ≤ k t)157 (hmono : MonotoneOn k (Ici (0 : ℝ))) :158 ENNReal.ofReal lowerConstant * (∑' n, sample k (n + 1)) ≤ smallIntegral k ∧159 smallIntegral k ≤ ENNReal.ofReal upperConstant * (∑' n, sample k n) := by160 rw [smallIntegral_eq_tsum, ← ENNReal.tsum_mul_left, ← ENNReal.tsum_mul_left]161 exact ⟨ENNReal.tsum_le_tsum (fun n => (shell_bounds hk hmono n).1),162 ENNReal.tsum_le_tsum (fun n => (shell_bounds hk hmono n).2)⟩163164theorem smallIntegral_ne_top_iff (hk : ∀ t ∈ Ici (0 : ℝ), 0 ≤ k t)165 (hmono : MonotoneOn k (Ici (0 : ℝ))) :166 smallIntegral k ≠ ⊤ ↔ (∑' n, sample k (n + 1)) ≠ ⊤ := by167 obtain ⟨hl, hu⟩ := smallIntegral_bounds hk hmono168 constructor169 · intro h hs170 have hc : ENNReal.ofReal lowerConstant ≠ 0 :=171 ne_of_gt (ENNReal.ofReal_pos.mpr lowerConstant_pos)172 simp [hs, hc, h] at hl173 · intro h174 apply ne_top_of_le_ne_top _ hu175 apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top176 rw [tsum_eq_zero_add' ENNReal.summable]177 exact ENNReal.add_ne_top.mpr ⟨ENNReal.ofReal_ne_top, h⟩178179theorem tailIntegral_eq {c : ℝ} (hc : 0 ≤ c)180 (htail : ∀ t, 1 ≤ t → k t = c) :181 (∫⁻ t in Ioi (1 : ℝ), integrand k t) = ENNReal.ofReal (2 * c) := by182 have heq : (∫⁻ t in Ioi (1 : ℝ), integrand k t) =183 ∫⁻ t in Ioi (1 : ℝ), ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * c) := by184 apply setLIntegral_congr_fun measurableSet_Ioi185 intro t ht186 rw [integrand, htail t ht.le]187 rw [heq]188 have hi := (integrableOn_Ioi_rpow_of_lt (by norm_num : (-3 / 2 : ℝ) < -1)189 (by norm_num : (0 : ℝ) < 1)).mul_const c190 have hn : 0 ≤ᵐ[volume.restrict (Ioi (1 : ℝ))] fun t => t ^ (-3 / 2 : ℝ) * c := by191 filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht192 change 1 < t at ht193 exact mul_nonneg (Real.rpow_nonneg (by linarith : 0 ≤ t) _) hc194 rw [← ofReal_integral_eq_lintegral_ofReal hi hn, integral_mul_const,195 integral_Ioi_rpow_of_lt (by norm_num : (-3 / 2 : ℝ) < -1) (by norm_num : (0 : ℝ) < 1)]196 norm_num197198theorem fullIntegral_eq {c : ℝ} (hc : 0 ≤ c)199 (htail : ∀ t, 1 ≤ t → k t = c) :200 fullIntegral k = smallIntegral k + ENNReal.ofReal (2 * c) := by201 have hs : Ioi (0 : ℝ) = Ioc 0 1 ∪ Ioi 1 := by202 ext t203 simp only [mem_Ioi, mem_union, mem_Ioc]204 constructor205 · intro ht206 by_cases h : t ≤ 1207 · exact Or.inl ⟨ht, h⟩208 · exact Or.inr (lt_of_not_ge h)209 · rintro (⟨ht, _⟩ | ht) <;> linarith210 have hd : Disjoint (Ioc (0 : ℝ) 1) (Ioi 1) := by211 rw [Set.disjoint_left]212 intro t ht ht'213 exact (not_lt_of_ge ht.2) ht'214 rw [fullIntegral, hs, lintegral_union measurableSet_Ioi hd, tailIntegral_eq hc htail]215 rfl216217theorem fullIntegral_ne_top_iff (hk : ∀ t ∈ Ici (0 : ℝ), 0 ≤ k t)218 (hmono : MonotoneOn k (Ici (0 : ℝ)))219 (htail : ∀ t, 1 ≤ t → k t = k 1) :220 fullIntegral k ≠ ⊤ ↔ (∑' n, sample k (n + 1)) ≠ ⊤ := by221 rw [fullIntegral_eq (hk 1 (by norm_num)) htail, ENNReal.add_ne_top]222 rw [and_iff_left ENNReal.ofReal_ne_top]223 exact smallIntegral_ne_top_iff hk hmono224225end PL1.DyadicInterpolation226227