PL1/IntervalDyadicApproximation.lean
All source files · Download exact source
SHA-256: 687d4fb58bd4ccb370c45cba290c54d8d1eac4d0f19dd378e0557f9fcb95a73e
1import PL1.DyadicTrace2import PL1.StrongConvergence3import PL1.PartitionAverages4import PL1.TraceDomination56/-! # Geometry and approximation by the concrete dyadic interval partitions -/78noncomputable section9set_option autoImplicit false10set_option maxHeartbeats 80000011open MeasureTheory Filter12open scoped ENNReal BigOperators Topology BoundedContinuousFunction1314namespace PL1.DyadicTrace1516attribute [local instance] intervalMeasure_probability1718theorem index_succ_div (n : ℕ) (x : ℝ) : index (n + 1) x / 2 = index n x := by19 unfold index20 have hfloor : ⌊(2 : ℝ) ^ (n + 1) * x⌋₊ / 2 = ⌊(2 : ℝ) ^ n * x⌋₊ := by21 rw [show (2 : ℝ) ^ (n + 1) * x = (2 ^ n * x) * 2 by rw [pow_succ]; ring]22 exact Nat.mul_cast_floor_div_cancel (by decide : (2 : ℕ) ≠ 0) _23 have hcap : (2 ^ (n + 1) - 1) / 2 = 2 ^ n - 1 := by24 rw [pow_succ]25 have hpos : 0 < (2 : ℕ) ^ n := pow_pos (by decide) n26 omega27 omega2829theorem cell_refine (n i : ℕ) : cell n i = cell (n + 1) (2 * i) ∪ cell (n + 1) (2 * i + 1) := by30 ext x31 have h := index_succ_div n x32 simp only [cell, Set.mem_ofPred_eq, Set.mem_union]33 omega3435theorem index_location (n : ℕ) (x : ℝ) (hx : x ∈ Set.Icc (0 : ℝ) 1) :36 (index n x : ℝ) ≤ (2 : ℝ) ^ n * x ∧37 (2 : ℝ) ^ n * x ≤ (index n x : ℝ) + 1 := by38 have hpos : 0 < (2 : ℝ) ^ n := pow_pos (by norm_num) n39 have hfloor := Nat.floor_le (mul_nonneg hpos.le hx.1)40 have hil : index n x ≤ ⌊(2 : ℝ) ^ n * x⌋₊ := min_le_left _ _41 have hil' : (index n x : ℝ) ≤ (⌊(2 : ℝ) ^ n * x⌋₊ : ℝ) := by exact_mod_cast hil42 refine ⟨hil'.trans hfloor, ?_⟩43 by_cases hi : ⌊(2 : ℝ) ^ n * x⌋₊ ≤ 2 ^ n - 144 · rw [index, min_eq_left hi]45 exact (Nat.lt_floor_add_one _).le46 · rw [index, min_eq_right (le_of_lt (lt_of_not_ge hi))]47 have hn : 1 ≤ (2 : ℕ) ^ n := Nat.one_le_iff_ne_zero.mpr (pow_ne_zero n (by decide))48 have hcast : ((2 ^ n - 1 : ℕ) : ℝ) + 1 = (2 : ℝ) ^ n := by49 rw [Nat.cast_sub hn, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one]50 ring51 rw [hcast]52 exact mul_le_of_le_one_right hpos.le hx.25354theorem dist_le_mesh (n i : ℕ) {x y : ℝ}55 (hx : x ∈ Set.Icc (0 : ℝ) 1) (hy : y ∈ Set.Icc (0 : ℝ) 1)56 (hxi : x ∈ cell n i) (hyi : y ∈ cell n i) : dist x y ≤ (2 : ℝ)⁻¹ ^ n := by57 have hxl := index_location n x hx58 have hyl := index_location n y hy59 change index n x = i at hxi60 change index n y = i at hyi61 rw [hxi] at hxl62 rw [hyi] at hyl63 have hpos : 0 < (2 : ℝ) ^ n := pow_pos (by norm_num) n64 rw [Real.dist_eq, abs_le, inv_pow]65 constructor66 · have h := (le_div_iff₀ hpos).mpr (show (y - x) * 2 ^ n ≤ 1 by nlinarith)67 rw [one_div] at h68 linarith69 · rw [← one_div]70 apply (le_div_iff₀ hpos).mpr71 nlinarith7273theorem left_mem_interval (n i : ℕ) (hi : i < 2 ^ n) :74 (i : ℝ) / (2 : ℝ) ^ n ∈ Set.Icc (0 : ℝ) 1 := by75 have hp : 0 < (2 : ℝ) ^ n := pow_pos (by norm_num) n76 refine ⟨by positivity, (div_le_one hp).mpr ?_⟩77 exact_mod_cast hi.le7879theorem index_left (n i : ℕ) (hi : i < 2 ^ n) :80 index n ((i : ℝ) / (2 : ℝ) ^ n) = i := by81 unfold index82 rw [mul_div_cancel₀ _ (pow_ne_zero n (by norm_num)), Nat.floor_natCast,83 min_eq_left (Nat.le_sub_one_of_lt hi)]8485variable {𝕜 : Type*} [RCLike 𝕜]8687abbrev dyadicVector (n i : ℕ) : IntervalL1 𝕜 :=88 PartitionAverages.vector intervalMeasure (cell n) (measurableSet_cell n) i8990def step (n : ℕ) (c : ℕ → 𝕜) : IntervalL1 𝕜 :=91 ∑ i ∈ Finset.range (2 ^ n), c i • dyadicVector (𝕜 := 𝕜) n i9293theorem coeFn_step (n : ℕ) (c : ℕ → 𝕜) :94 step n c =ᵐ[intervalMeasure] (fun x => c (index n x)) := by95 refine (Lp.coeFn_fun_finsetSum (Finset.range (2 ^ n)) _).trans ?_96 filter_upwards [ae_all_iff.2 (fun i => Lp.coeFn_smul (c i) (dyadicVector (𝕜 := 𝕜) n i)),97 ae_all_iff.2 (fun i => indicatorConstLp_coeFn (p := 1) (hs := measurableSet_cell n i)98 (hμs := measure_ne_top intervalMeasure (cell n i)) (c := (1 : 𝕜)))] with x hs he99 rw [Finset.sum_eq_single (index n x)]100 · rw [hs (index n x)]101 change c (index n x) * dyadicVector (𝕜 := 𝕜) n (index n x) x = _102 rw [show dyadicVector (𝕜 := 𝕜) n (index n x) x = (cell n (index n x)).indicator (fun _ => (1 : 𝕜)) x103 from he (index n x), Set.indicator_of_mem (show x ∈ cell n (index n x) from rfl), mul_one]104 · intro i hi hix105 rw [hs i]106 change c i * dyadicVector (𝕜 := 𝕜) n i x = _107 rw [show dyadicVector (𝕜 := 𝕜) n i x = (cell n i).indicator (fun _ => (1 : 𝕜)) x from he i,108 Set.indicator_of_notMem (show x ∉ cell n i from fun h => hix h.symm), mul_zero]109 · intro h110 exact (h (Finset.mem_range.mpr (index_lt n x))).elim111112abbrev dyadicAverage (n : ℕ) : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜 :=113 PartitionAverages.average intervalMeasure (cell n) (measurableSet_cell n) (Finset.range (2 ^ n))114115theorem norm_dyadicAverage_le_one (n : ℕ) : ‖dyadicAverage (𝕜 := 𝕜) n‖ ≤ 1 :=116 PartitionAverages.norm_average_le_one _ _ _ _ (pairwiseDisjoint_cell n)117118theorem dyadicAverage_step (n : ℕ) (c : ℕ → 𝕜) : dyadicAverage n (step n c) = step n c :=119 PartitionAverages.average_step _ _ _ _ (pairwiseDisjoint_cell n) c120121theorem step_continuous_tendsto (f : ℝ →ᵇ 𝕜) :122 Tendsto (fun n => step n (fun i => f ((i : ℝ) / (2 : ℝ) ^ n))) atTop123 (𝓝 (BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 f)) := by124 apply Metric.tendsto_atTop.mpr125 intro ε hε126 obtain ⟨δ, hδ, hfδ⟩ := Metric.uniformContinuousOn_iff.mp127 ((isCompact_Icc : IsCompact (Set.Icc (0 : ℝ) 1)).uniformContinuousOn_of_continuous128 f.continuous.continuousOn)129 (ε / 2) (half_pos hε)130 have hmesh : Tendsto (fun n : ℕ => (2 : ℝ)⁻¹ ^ n) atTop (𝓝 0) :=131 tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num)132 obtain ⟨N, hN⟩ := eventually_atTop.mp (hmesh.eventually (gt_mem_nhds hδ))133 refine ⟨N, fun n hn => ?_⟩134 rw [dist_eq_norm]135 have hmem : ∀ᵐ x ∂intervalMeasure, x ∈ Set.Icc (0 : ℝ) 1 :=136 ae_restrict_mem measurableSet_Icc137 have hb : ∀ᵐ x ∂intervalMeasure,138 ‖(step n (fun i => f ((i : ℝ) / (2 : ℝ) ^ n)) -139 BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 f) x‖ ≤ ε / 2 := by140 filter_upwards [Lp.coeFn_sub (step n (fun i => f ((i : ℝ) / (2 : ℝ) ^ n)))141 (BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 f), coeFn_step n142 (fun i => f ((i : ℝ) / (2 : ℝ) ^ n)), BoundedContinuousFunction.coeFn_toLp 1 intervalMeasure 𝕜 f,143 hmem] with x hsub hs hf hx144 rw [hsub, Pi.sub_apply, hs, hf]145 have hleft := left_mem_interval n (index n x) (index_lt n x)146 have hdist := dist_le_mesh n (index n x) hleft hx147 (index_left n (index n x) (index_lt n x)) rfl148 simpa only [dist_eq_norm] using (hfδ _ hleft x hx (hdist.trans_lt (hN n hn))).le149 have hnorm := Lp.norm_le_of_ae_bound (half_pos hε).le hb150 have hnorm' : ‖step n (fun i => f ((i : ℝ) / (2 : ℝ) ^ n)) -151 BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 f‖ ≤ ε / 2 := by152 simpa [measureUnivNNReal] using hnorm153 exact hnorm'.trans_lt (half_lt_self hε)154155set_option backward.isDefEq.respectTransparency false in156theorem dyadicAverage_continuous_tendsto (f : ℝ →ᵇ 𝕜) :157 Tendsto (fun n => dyadicAverage n (BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 f))158 atTop (𝓝 (BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 f)) := by159 let F := BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 f160 let v : ℕ → IntervalL1 𝕜 := fun n => step n (fun i => f ((i : ℝ) / (2 : ℝ) ^ n))161 have hv : Tendsto v atTop (𝓝 F) := step_continuous_tendsto f162 have hb (n : ℕ) : ‖dyadicAverage n F - F‖ ≤ 2 * ‖v n - F‖ := by163 have heq : dyadicAverage n F - F = dyadicAverage n (F - v n) + (v n - F) := by164 rw [map_sub, show dyadicAverage n (v n) = v n from dyadicAverage_step n _]165 abel166 rw [heq]167 calc168 _ ≤ ‖dyadicAverage n (F - v n)‖ + ‖v n - F‖ := norm_add_le _ _169 _ ≤ ‖F - v n‖ + ‖v n - F‖ := by170 have hnorm : ‖dyadicAverage n (F - v n)‖ ≤ ‖F - v n‖ := by171 calc172 ‖dyadicAverage n (F - v n)‖ ≤ ‖dyadicAverage (𝕜 := 𝕜) n‖ * ‖F - v n‖ :=173 ContinuousLinearMap.le_opNorm (dyadicAverage (𝕜 := 𝕜) n) (F - v n)174 _ ≤ 1 * ‖F - v n‖ := mul_le_mul_of_nonneg_right175 (norm_dyadicAverage_le_one (𝕜 := 𝕜) n) (norm_nonneg _)176 _ = ‖F - v n‖ := one_mul _177 linarith178 _ = 2 * ‖v n - F‖ := by rw [norm_sub_rev F (v n)]; ring179 apply tendsto_iff_norm_sub_tendsto_zero.mpr180 have hzero : Tendsto (fun n => 2 * ‖v n - F‖) atTop (𝓝 0) := by181 simpa using (hv.sub_const F).norm.const_mul 2182 exact squeeze_zero (fun _ => norm_nonneg _) hb hzero183184theorem dyadicAverage_tendsto (f : IntervalL1 𝕜) :185 Tendsto (fun n => dyadicAverage n f) atTop (𝓝 f) := by186 have hclosed := isClosed_convergenceSubmodule (dyadicAverage (𝕜 := 𝕜))187 (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜)) atTop 1 norm_dyadicAverage_le_one188 have hsubset : Set.range (BoundedContinuousFunction.toLp 1 intervalMeasure 𝕜 :189 (ℝ →ᵇ 𝕜) →L[𝕜] IntervalL1 𝕜) ⊆190 convergenceSubmodule (dyadicAverage (𝕜 := 𝕜)) (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜)) atTop := by191 rintro g ⟨v, rfl⟩192 exact dyadicAverage_continuous_tendsto v193 have hdense := BoundedContinuousFunction.toLp_denseRange 𝕜 intervalMeasure 𝕜 (p := 1) (by norm_num)194 exact hclosed.closure_subset_iff.mpr hsubset (hdense f)195196theorem dyadicVector_refine (n i : ℕ) :197 dyadicVector (𝕜 := 𝕜) n i = dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i) +198 dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i + 1) := by199 apply Lp.ext200 filter_upwards [Lp.coeFn_add (dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i))201 (dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i + 1)),202 indicatorConstLp_coeFn (p := 1) (hs := measurableSet_cell n i)203 (hμs := measure_ne_top intervalMeasure (cell n i)) (c := (1 : 𝕜)),204 indicatorConstLp_coeFn (p := 1) (hs := measurableSet_cell (n + 1) (2 * i))205 (hμs := measure_ne_top intervalMeasure (cell (n + 1) (2 * i))) (c := (1 : 𝕜)),206 indicatorConstLp_coeFn (p := 1) (hs := measurableSet_cell (n + 1) (2 * i + 1))207 (hμs := measure_ne_top intervalMeasure (cell (n + 1) (2 * i + 1))) (c := (1 : 𝕜))]208 with x hadd hp h0 h1209 change dyadicVector (𝕜 := 𝕜) n i x = _210 rw [hadd]211 change dyadicVector (𝕜 := 𝕜) n i x = dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i) x +212 dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i + 1) x213 rw [show dyadicVector (𝕜 := 𝕜) n i x = _ from hp,214 show dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i) x = _ from h0,215 show dyadicVector (𝕜 := 𝕜) (n + 1) (2 * i + 1) x = _ from h1,216 cell_refine]217 have hdisj : Disjoint (cell (n + 1) (2 * i)) (cell (n + 1) (2 * i + 1)) :=218 pairwiseDisjoint_cell (n + 1) (by omega)219 exact congrFun (Set.indicator_union_of_disjoint hdisj (fun _ => (1 : 𝕜))) x220221theorem sum_norm_dyadicVector (n : ℕ) :222 (∑ i ∈ Finset.range (2 ^ n), ‖dyadicVector (𝕜 := 𝕜) n i‖) = 1 := by223 simp only [dyadicVector, PartitionAverages.norm_vector]224 rw [← measureReal_biUnion_finset (fun i _ j _ hij => pairwiseDisjoint_cell n hij)225 (fun i _ => measurableSet_cell n i) (fun i _ => measure_ne_top intervalMeasure (cell n i)), cover_cell]226 simp227228/-- The full trace-dominator lemma, for arbitrary real or complex operators229and arbitrary (possibly infinite) target measure. -/230theorem exists_integrable_dominator {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)231 (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ) :232 ∃ G : Ω → ℝ, Integrable G μ ∧ (∀ x, 0 ≤ G x) ∧ (∫ x, G x ∂μ) ≤ ‖B‖ ∧233 ∀ f : Lp 𝕜 ∞ intervalMeasure, ‖f‖ ≤ 1 →234 ∀ᵐ x ∂μ, ‖B (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top f) x‖ ≤ G x := by235 let U : Set (IntervalL1 𝕜) := {g | ∃ f : Lp 𝕜 ∞ intervalMeasure,236 ‖f‖ ≤ 1 ∧ ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top f = g}237 have happrox : ∀ g ∈ U, ∃ c : ℕ → ℕ → 𝕜, (∀ n i, ‖c n i‖ ≤ 1) ∧238 Tendsto (fun n => ∑ i ∈ Finset.range (2 ^ n), c n i • dyadicVector (𝕜 := 𝕜) n i)239 atTop (𝓝 g) := by240 rintro g ⟨f, hf, rfl⟩241 refine ⟨fun n i => PartitionAverages.coefficient intervalMeasure (cell n) (measurableSet_cell n) i242 (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top f), ?_, ?_⟩243 · intro n i244 exact PartitionAverages.norm_coefficient_inclusion_le_one _ _ _ i f hf245 · simpa only [dyadicAverage, PartitionAverages.average_apply] using246 dyadicAverage_tendsto (ProbabilityLp.inclusion intervalMeasure 1 ∞ le_top f)247 obtain ⟨G, hG, hGpos, hGint, hGU⟩ := TraceDomination.exists_dominator_of_binary_approximation μ248 (dyadicVector (𝕜 := 𝕜)) B (fun n i _ => dyadicVector_refine n i)249 (fun n => (sum_norm_dyadicVector (𝕜 := 𝕜) n).le) U happrox250 exact ⟨G, hG, hGpos, hGint, fun f hf => hGU _ ⟨f, hf, rfl⟩⟩251252end PL1.DyadicTrace253254