PL1/SingularCarrier.lean
All source files · Download exact source
SHA-256: b1cbc5913d7fc56a181659c4ecd9c7ec34ad1923edb68081e12e6471738d539a
1import PL1.NoiseMeasures2import PL1.CarrierAsymptotics3import Mathlib.Probability.Moments.Variance4import Mathlib.Probability.Independence.InfinitePi5import Mathlib.MeasureTheory.OuterMeasure.BorelCantelli67/-!8# Common singular carriers from coordinate averages910The coordinate random variables and noise measures below are the actual sign11product model. The general Borel–Cantelli lemma keeps the summability inputs12explicit; the subsequent moment calculations discharge the probabilistic13ingredients for the concrete coordinate averages.14-/1516noncomputable section17open MeasureTheory ProbabilityTheory Filter18open scoped Topology BigOperators ENNReal NNReal1920namespace PL1.Carrier2122section BorelCantelli2324variable {Ω : Type*} [MeasurableSpace Ω]2526/-- The set of points belonging to all sufficiently late events. -/27def eventualSet (A : ℕ → Set Ω) : Set Ω := liminf A atTop2829theorem measurableSet_eventualSet {A : ℕ → Set Ω} (hA : ∀ n, MeasurableSet (A n)) :30 MeasurableSet (eventualSet A) :=31 MeasurableSet.measurableSet_liminf hA3233/-- Summable event probabilities make the eventual-event carrier null. -/34theorem measure_eventualSet_eq_zero (μ : Measure Ω) (A : ℕ → Set Ω)35 (hA : (∑' n, μ (A n)) ≠ ∞) : μ (eventualSet A) = 0 :=36 measure_liminf_atTop_eq_zero hA3738/-- Summable complementary-event probabilities make the same carrier full. -/39theorem measure_eventualSet_eq_one (μ : Measure Ω) [IsProbabilityMeasure μ]40 (A : ℕ → Set Ω) (hA : ∀ n, MeasurableSet (A n))41 (hcompl : (∑' n, μ (A n)ᶜ) ≠ ∞) : μ (eventualSet A) = 1 := by42 apply (mem_ae_iff_prob_eq_one (measurableSet_eventualSet hA)).mp43 filter_upwards [ae_eventually_notMem hcompl] with x hx44 change x ∈ liminf A atTop45 rw [mem_liminf_iff_eventually_mem]46 simpa only [Set.mem_compl_iff, not_not] using hx4748/-- A useful one-sided Chebyshev bound for an event above a zero mean. -/49theorem measure_above_le (μ : Measure Ω) [IsProbabilityMeasure μ]50 (X : Ω → ℝ) (hX : MemLp X 2 μ) (hmean : ∫ x, X x ∂μ = 0)51 {a : ℝ} (ha : 0 < a) :52 μ {x | a < X x} ≤ ENNReal.ofReal (variance X μ / a ^ 2) := by53 apply le_trans (measure_mono ?_) (meas_ge_le_variance_div_sq hX ha)54 intro x hx55 change a ≤ |X x - ∫ y, X y ∂μ|56 rw [hmean, sub_zero]57 exact hx.le.trans (le_abs_self _)5859/-- A lower-tail Chebyshev estimate when the mean exceeds twice the threshold. -/60theorem measure_below_le (μ : Measure Ω) [IsProbabilityMeasure μ]61 (X : Ω → ℝ) (hX : MemLp X 2 μ) {a b : ℝ}62 (hmean : b ≤ ∫ x, X x ∂μ) (hb : 0 < b) (hab : 2 * a ≤ b) :63 μ {x | X x ≤ a} ≤ ENNReal.ofReal (variance X μ / (b / 2) ^ 2) := by64 apply le_trans (measure_mono ?_) (meas_ge_le_variance_div_sq hX (half_pos hb))65 intro x hx66 change X x ≤ a at hx67 change b / 2 ≤ |X x - ∫ y, X y ∂μ|68 have h := neg_le_abs (X x - ∫ y, X y ∂μ)69 linarith7071/-- An eventual summable real upper bound suffices for finite total event mass;72the finitely many early events are finite because the ambient measure is. -/73theorem tsum_measure_ne_top_of_eventually_le (μ : Measure Ω) [IsFiniteMeasure μ]74 (A : ℕ → Set Ω) (f : ℕ → ℝ) (hf : Summable f) (hf0 : ∀ n, 0 ≤ f n)75 (hA : ∀ᶠ n : ℕ in atTop, μ (A n) ≤ ENNReal.ofReal (f n)) :76 (∑' n, μ (A n)) ≠ ∞ := by77 have hreal : Summable (fun n : ℕ => (μ (A n)).toReal) := by78 apply hf.of_norm_bounded_eventually_nat79 filter_upwards [hA] with n hn80 rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]81 exact ENNReal.toReal_le_of_le_ofReal (hf0 n) hn82 have hfinite := hreal.tsum_ofReal_ne_top83 simpa only [ENNReal.ofReal_toReal (measure_ne_top _ _)] using hfinite8485end BorelCantelli8687open Walsh8889/-- A real sign-valued coordinate random variable. -/90def coordinate (j : ℕ) (x : Walsh.Group) : ℝ := signValue (x j)9192theorem continuous_coordinate (j : ℕ) : Continuous (coordinate j) := by93 change Continuous (fun x : Walsh.Group => signValue (x j))94 exact (continuous_of_discreteTopology : Continuous signValue).comp (continuous_apply j)9596theorem memLp_coordinate (μ : Measure Walsh.Group) [IsFiniteMeasure μ]97 (j : ℕ) (p : ℝ≥0∞) : MemLp (coordinate j) p μ := by98 apply MemLp.of_bound (continuous_coordinate j).aestronglyMeasurable 199 filter_upwards [] with x100 exact (norm_signValue (x j)).le101102theorem integral_coordinate_haar (j : ℕ) : ∫ x, coordinate j x ∂haar = 0 := by103 simpa only [coordinate, character_singleton] using104 integral_character_eq_zero (Finset.singleton_nonempty j)105106theorem integral_coordinate_noise (rates : ℕ → ℝ≥0) (u : ℝ≥0) (j : ℕ) :107 ∫ x, coordinate j x ∂Noise.measure rates u = Noise.bias rates u j := by108 simpa only [coordinate, character_singleton, Noise.rateSum, Finset.sum_singleton, Noise.bias] using109 Noise.integral_character rates u {j}110111theorem variance_coordinate_le_one (μ : Measure Walsh.Group) [IsProbabilityMeasure μ]112 (j : ℕ) : variance (coordinate j) μ ≤ 1 := by113 rw [variance_eq_sub (memLp_coordinate μ j 2)]114 have hsq : coordinate j ^ (2 : ℕ) = fun _ => (1 : ℝ) := by115 funext x116 change signValue (x j) ^ 2 = 1117 rw [pow_two, signValue_mul_self]118 rw [hsq]119 simp only [integral_const, probReal_univ, smul_eq_mul, one_mul]120 exact sub_le_self _ (sq_nonneg _)121122theorem covariance_coordinate_haar {i j : ℕ} (hij : i ≠ j) :123 covariance (coordinate i) (coordinate j) haar = 0 := by124 rw [covariance_eq_sub (memLp_coordinate haar i 2) (memLp_coordinate haar j 2)]125 simp only [integral_coordinate_haar, zero_mul, sub_zero]126 simpa [coordinate, Pi.mul_apply, hij] using integral_character_mul {i} {j}127128theorem covariance_coordinate_noise (rates : ℕ → ℝ≥0) (u : ℝ≥0)129 {i j : ℕ} (hij : i ≠ j) :130 covariance (coordinate i) (coordinate j) (Noise.measure rates u) = 0 := by131 have h := iIndepFun_infinitePi (P := Noise.coordinateMeasure rates u)132 (X := fun _ : ℕ => signValue) (fun _ => continuous_of_discreteTopology.measurable)133 exact (h.indepFun hij).covariance_eq_zero134 (memLp_coordinate (Noise.measure rates u) i 2)135 (memLp_coordinate (Noise.measure rates u) j 2)136137/-- Pairwise uncorrelated, square-integrable summands with variance at most one138have sum variance at most their number. -/139theorem variance_sum_le_card {Ω : Type*} [MeasurableSpace Ω]140 (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (F : Finset ℕ)141 (hX : ∀ i ∈ F, MemLp (X i) 2 μ)142 (hvar : ∀ i ∈ F, variance (X i) μ ≤ 1)143 (hcov : ∀ i ∈ F, ∀ j ∈ F, i ≠ j → covariance (X i) (X j) μ = 0) :144 variance (∑ i ∈ F, X i) μ ≤ F.card := by145 rw [variance_sum' hX]146 calc147 (∑ i ∈ F, ∑ j ∈ F, covariance (X i) (X j) μ) =148 ∑ i ∈ F, variance (X i) μ := by149 apply Finset.sum_congr rfl150 intro i hi151 rw [Finset.sum_eq_single_of_mem i hi]152 · exact covariance_self (hX i hi).aemeasurable153 · intro j hj hji154 exact hcov i hi j hj hji.symm155 _ ≤ ∑ i ∈ F, (1 : ℝ) := Finset.sum_le_sum hvar156 _ = F.card := by simp157158/-- The dyadic coordinate averages, also allowing deletion of an initial segment. -/159def average (d r : ℕ) (x : Walsh.Group) : ℝ :=160 ((2 : ℝ) ^ r)⁻¹ * ∑ j ∈ Finset.range (2 ^ r), coordinate (d + j) x161162theorem continuous_average (d r : ℕ) : Continuous (average d r) := by163 unfold average164 apply continuous_const.mul165 apply continuous_finsetSum166 intro j hj167 exact continuous_coordinate _168169theorem memLp_average (μ : Measure Walsh.Group) [IsFiniteMeasure μ] (d r : ℕ) :170 MemLp (average d r) 2 μ := by171 apply (memLp_finsetSum (Finset.range (2 ^ r))172 (fun j _ => memLp_coordinate μ (d + j) 2)).const_mul173174theorem integral_average_haar (d r : ℕ) : ∫ x, average d r x ∂haar = 0 := by175 unfold average176 rw [integral_const_mul, integral_finsetSum]177 · simp only [integral_coordinate_haar, Finset.sum_const_zero, mul_zero]178 · intro j hj179 exact (memLp_coordinate haar (d + j) 2).integrable (by norm_num)180181theorem integral_average_noise (rates : ℕ → ℝ≥0) (u : ℝ≥0) (d r : ℕ) :182 ∫ x, average d r x ∂Noise.measure rates u =183 ((2 : ℝ) ^ r)⁻¹ * ∑ j ∈ Finset.range (2 ^ r), Noise.bias rates u (d + j) := by184 unfold average185 rw [integral_const_mul, integral_finsetSum]186 · simp only [integral_coordinate_noise]187 · intro j hj188 exact (memLp_coordinate (Noise.measure rates u) (d + j) 2).integrable (by norm_num)189190theorem variance_average_le (μ : Measure Walsh.Group) [IsProbabilityMeasure μ] (d r : ℕ)191 (hcov : ∀ i j : ℕ, i ≠ j → covariance (coordinate i) (coordinate j) μ = 0) :192 variance (average d r) μ ≤ (1 / 2 : ℝ) ^ r := by193 have hsum := variance_sum_le_card μ (fun j => coordinate (d + j)) (Finset.range (2 ^ r))194 (fun j _ => memLp_coordinate μ (d + j) 2)195 (fun j _ => variance_coordinate_le_one μ (d + j))196 (fun i _ j _ hij => hcov _ _ (by omega))197 simp only [Finset.card_range, Nat.cast_pow, Nat.cast_ofNat] at hsum198 have havg : average d r =199 ((2 : ℝ) ^ r)⁻¹ • ∑ j ∈ Finset.range (2 ^ r), coordinate (d + j) := by200 funext x201 simp only [average, Pi.smul_apply, Finset.sum_apply, smul_eq_mul]202 rw [havg, variance_smul]203 calc204 (((2 : ℝ) ^ r)⁻¹) ^ 2 *205 variance (∑ j ∈ Finset.range (2 ^ r), coordinate (d + j)) μ206 ≤ (((2 : ℝ) ^ r)⁻¹) ^ 2 * (2 : ℝ) ^ r :=207 mul_le_mul_of_nonneg_left hsum (sq_nonneg _)208 _ = (1 / 2 : ℝ) ^ r := by209 have hne : (2 : ℝ) ^ r ≠ 0 := by positivity210 rw [one_div_pow, sq]211 field_simp212213theorem variance_average_haar_le (d r : ℕ) :214 variance (average d r) haar ≤ (1 / 2 : ℝ) ^ r :=215 variance_average_le haar d r (fun _ _ hij => covariance_coordinate_haar hij)216217theorem variance_average_noise_le (rates : ℕ → ℝ≥0) (u : ℝ≥0) (d r : ℕ) :218 variance (average d r) (Noise.measure rates u) ≤ (1 / 2 : ℝ) ^ r :=219 variance_average_le (Noise.measure rates u) d r220 (fun _ _ hij => covariance_coordinate_noise rates u hij)221222open CarrierAsymptotics223224/-- The open coordinate-average events defining the common carrier. -/225def highEvent (d r : ℕ) : Set Walsh.Group := {x | threshold r < average d r x}226227/-- One Borel set for each deleted finite prefix, independent of noise time. -/228def commonSet (d : ℕ) : Set Walsh.Group := eventualSet (highEvent d)229230theorem measurableSet_highEvent (d r : ℕ) : MeasurableSet (highEvent d r) :=231 measurableSet_lt measurable_const (continuous_average d r).measurable232233theorem measurableSet_commonSet (d : ℕ) : MeasurableSet (commonSet d) :=234 measurableSet_eventualSet (measurableSet_highEvent d)235236theorem haar_highEvent_le (d r : ℕ) :237 haar (highEvent d r) ≤ ENNReal.ofReal ((1 / 2 : ℝ) ^ r / (threshold r) ^ 2) := by238 apply (measure_above_le haar (average d r) (memLp_average haar d r)239 (integral_average_haar d r) (threshold_pos r)).trans240 apply ENNReal.ofReal_le_ofReal241 exact div_le_div_of_nonneg_right (variance_average_haar_le d r) (sq_nonneg _)242243/-- The same carrier is Haar-null after deleting any finite number of coordinates. -/244theorem haar_commonSet_eq_zero (d : ℕ) : haar (commonSet d) = 0 := by245 apply measure_eventualSet_eq_zero246 exact ne_top_of_le_ne_top summable_haar_failure_bound.tsum_ofReal_ne_top247 (ENNReal.tsum_le_tsum (haar_highEvent_le d))248249theorem bias_schurRates_ge (u : ℝ≥0) (d r j : ℕ) (hj : j < 2 ^ r) :250 biasLower u ((d : ℝ) + 1) r ≤ Noise.bias Noise.schurRates u (d + j) := by251 apply Real.exp_le_exp.mpr252 change -(u : ℝ) * Real.sqrt (((r : ℝ) + ((d : ℝ) + 1)) * Real.log 2) ≤253 -(u : ℝ) * Real.sqrt (Real.log ((d + j : ℕ) + 2 : ℝ))254 have h := mul_le_mul_of_nonpos_left (shifted_rate_le d r j hj)255 (neg_nonpos.mpr u.coe_nonneg)256 simpa only [add_assoc] using h257258theorem integral_average_schurRates_ge (u : ℝ≥0) (d r : ℕ) :259 biasLower u ((d : ℝ) + 1) r ≤ ∫ x, average d r x ∂Noise.measure Noise.schurRates u := by260 rw [integral_average_noise]261 have hsum : (2 : ℝ) ^ r * biasLower u ((d : ℝ) + 1) r ≤262 ∑ j ∈ Finset.range (2 ^ r), Noise.bias Noise.schurRates u (d + j) := by263 calc264 _ = ∑ _j ∈ Finset.range (2 ^ r), biasLower u ((d : ℝ) + 1) r := by simp265 _ ≤ _ := Finset.sum_le_sum (fun j hj =>266 bias_schurRates_ge u d r j (Finset.mem_range.mp hj))267 have hp : (2 : ℝ) ^ r ≠ 0 := by positivity268 calc269 biasLower u ((d : ℝ) + 1) r =270 ((2 : ℝ) ^ r)⁻¹ * ((2 : ℝ) ^ r * biasLower u ((d : ℝ) + 1) r) := by271 rw [← mul_assoc, inv_mul_cancel₀ hp, one_mul]272 _ ≤ _ := mul_le_mul_of_nonneg_left hsum (by positivity)273274theorem eventually_noise_highEvent_compl_le (u : ℝ≥0) (d : ℕ) :275 ∀ᶠ r : ℕ in atTop, Noise.measure Noise.schurRates u (highEvent d r)ᶜ ≤276 ENNReal.ofReal (4 * (1 / 2 : ℝ) ^ r *277 Real.exp (2 * (u : ℝ) * Real.sqrt (((r : ℝ) + ((d : ℝ) + 1)) * Real.log 2))) := by278 filter_upwards [eventually_two_threshold_le_biasLower u u.coe_nonneg279 ((d : ℝ) + 1) (by positivity)] with r hr280 have heq : (highEvent d r)ᶜ = {x | average d r x ≤ threshold r} := by281 ext x282 simp only [highEvent, Set.mem_compl_iff, Set.mem_ofPred_eq, not_lt]283 rw [heq]284 apply (measure_below_le (Noise.measure Noise.schurRates u) (average d r)285 (memLp_average (Noise.measure Noise.schurRates u) d r)286 (integral_average_schurRates_ge u d r) (biasLower_pos _ _ _) hr).trans287 apply ENNReal.ofReal_le_ofReal288 calc289 _ ≤ (1 / 2 : ℝ) ^ r / (biasLower u ((d : ℝ) + 1) r / 2) ^ 2 :=290 div_le_div_of_nonneg_right (variance_average_noise_le Noise.schurRates u d r)291 (sq_nonneg _)292 _ = _ := noise_failure_bound_eq u ((d : ℝ) + 1) r293294/-- The concrete common Borel carrier carries every product noise measure for295the Schur rates, including time zero, after any deleted finite prefix. -/296theorem noise_commonSet_eq_one (u : ℝ≥0) (d : ℕ) :297 Noise.measure Noise.schurRates u (commonSet d) = 1 := by298 apply measure_eventualSet_eq_one _ _ (measurableSet_highEvent d)299 apply tsum_measure_ne_top_of_eventually_le _ _300 (fun r : ℕ => 4 * (1 / 2 : ℝ) ^ r *301 Real.exp (2 * (u : ℝ) * Real.sqrt (((r : ℝ) + ((d : ℝ) + 1)) * Real.log 2)))302 (summable_noise_failure_bound u u.coe_nonneg ((d : ℝ) + 1) (by positivity))303 · intro r304 positivity305 · exact eventually_noise_highEvent_compl_le u d306307/-- The carrier genuinely depends only on the coordinates remaining after the308deleted prefix. -/309theorem mem_commonSet_iff_of_tail_eq (d : ℕ) {x y : Walsh.Group}310 (hxy : ∀ j : ℕ, x (d + j) = y (d + j)) :311 x ∈ commonSet d ↔ y ∈ commonSet d := by312 have havg (r : ℕ) : average d r x = average d r y := by313 unfold average314 congr 1315 apply Finset.sum_congr rfl316 intro j hj317 exact congrArg signValue (hxy j)318 simp only [commonSet, eventualSet, mem_liminf_iff_eventually_mem,319 highEvent, Set.mem_ofPred_eq, havg]320321theorem integral_average_constantRates (u : ℝ≥0) (d r : ℕ) :322 ∫ x, average d r x ∂Noise.measure Noise.constantRates u = Real.exp (-(u : ℝ)) := by323 rw [integral_average_noise]324 simp only [Noise.bias, Noise.constantRates, NNReal.coe_one, mul_one,325 Finset.sum_const, Finset.card_range, nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat]326 rw [← mul_assoc, inv_mul_cancel₀ (by positivity : (2 : ℝ) ^ r ≠ 0), one_mul]327328theorem threshold_tendsto_zero : Tendsto threshold atTop (𝓝 0) := by329 apply tendsto_pow_atTop_nhds_zero_of_lt_one (Real.exp_pos _).le330 apply Real.exp_lt_one_iff.mpr331 linarith [log_two_pos]332333/-- The same concrete carrier also carries every constant-rate product law. -/334theorem noise_constantRates_commonSet_eq_one (u : ℝ≥0) (d : ℕ) :335 Noise.measure Noise.constantRates u (commonSet d) = 1 := by336 have hpos : 0 < Real.exp (-(u : ℝ)) := Real.exp_pos _337 have hthreshold : ∀ᶠ r : ℕ in atTop, 2 * threshold r ≤ Real.exp (-(u : ℝ)) := by338 filter_upwards [threshold_tendsto_zero.eventually_lt_const (half_pos hpos)] with r hr339 linarith340 have hgeom : Summable (fun r : ℕ => (1 / 2 : ℝ) ^ r) :=341 summable_geometric_of_norm_lt_one (by norm_num)342 apply measure_eventualSet_eq_one _ _ (measurableSet_highEvent d)343 apply tsum_measure_ne_top_of_eventually_le _ _344 (fun r : ℕ => (1 / 2 : ℝ) ^ r / (Real.exp (-(u : ℝ)) / 2) ^ 2)345 (hgeom.div_const _)346 · intro r347 positivity348 · filter_upwards [hthreshold] with r hr349 have heq : (highEvent d r)ᶜ = {x | average d r x ≤ threshold r} := by350 ext x351 simp only [highEvent, Set.mem_compl_iff, Set.mem_ofPred_eq, not_lt]352 rw [heq]353 apply (measure_below_le (Noise.measure Noise.constantRates u) (average d r)354 (memLp_average (Noise.measure Noise.constantRates u) d r)355 (integral_average_constantRates u d r).ge hpos hr).trans356 apply ENNReal.ofReal_le_ofReal357 exact div_le_div_of_nonneg_right (variance_average_noise_le Noise.constantRates u d r)358 (sq_nonneg _)359360/-- Lemma 3.1 for the actual Schur-rate product probabilities, with one Borel361Haar-null set independent of time and with arbitrary finite-prefix deletion. -/362theorem exists_common_haar_null_carrier (d : ℕ) :363 ∃ N : Set Walsh.Group, MeasurableSet N ∧ haar N = 0 ∧364 ∀ u : ℝ≥0, Noise.measure Noise.schurRates u N = 1 :=365 ⟨commonSet d, measurableSet_commonSet d, haar_commonSet_eq_zero d,366 fun u => noise_commonSet_eq_one u d⟩367368/-- A single tail-dependent Borel Haar-null set works for both rate choices in369the paper, uniformly over every nonnegative time. -/370theorem exists_common_haar_null_carrier_both_rates (d : ℕ) :371 ∃ N : Set Walsh.Group, MeasurableSet N ∧ haar N = 0 ∧372 (∀ x y : Walsh.Group, (∀ j : ℕ, x (d + j) = y (d + j)) → (x ∈ N ↔ y ∈ N)) ∧373 (∀ u : ℝ≥0, Noise.measure Noise.schurRates u N = 1) ∧374 ∀ u : ℝ≥0, Noise.measure Noise.constantRates u N = 1 :=375 ⟨commonSet d, measurableSet_commonSet d, haar_commonSet_eq_zero d,376 fun _ _ h => mem_commonSet_iff_of_tail_eq d h,377 fun u => noise_commonSet_eq_one u d, fun u => noise_constantRates_commonSet_eq_one u d⟩378379end PL1.Carrier380