PL1/ConstantTailSpikes.lean

All source files · Download exact source

SHA-256: 4371c7ce385c3a90ab268f5009d986784555e8be1728dd444a3a32efe1bf0f05

1import PL1.TailSpikes23/-!4# Finite tail spikes for the constant-rate construction56The same actual coordinate-average events concentrate every probability7measure carried by the displayed common singular carrier. In particular,8they concentrate the constant-rate resolvent as well as the Schur resolvent.9-/1011noncomputable section12open MeasureTheory Filter13open scoped Topology ENNReal NNReal1415namespace PL1.TailSpikeEvents16open Walsh Carrier CarrierAsymptotics Noise FiniteCoordinateKernels1718theorem tendsto_probability_highEvent_of_commonSet (ν : Measure Walsh.Group)19    [IsProbabilityMeasure ν] (d : ℕ) (hν : ν (commonSet d) = 1) :20    Tendsto (fun r => ν.real (highEvent d r)) atTop (𝓝 1) := by21  have hae : ∀ᵐ x ∂ν, x ∈ commonSet d :=22    (mem_ae_iff_prob_eq_one (measurableSet_commonSet d)).mpr hν23  have hlim : Tendsto (fun r => ∫ x, (highEvent d r).indicator (fun _ => (1 : ℝ)) x ∂ν)24      atTop (𝓝 (∫ _x, (1 : ℝ) ∂ν)) := by25    apply tendsto_integral_of_dominated_convergence (fun _ => (1 : ℝ))26    · intro r27      exact (measurable_const.indicator (measurableSet_highEvent d r)).aestronglyMeasurable28    · exact integrable_const 129    · intro r30      exact ae_of_all _ (fun x => by31        by_cases hx : x ∈ highEvent d r <;> simp [hx])32    · filter_upwards [hae] with x hx33      change x ∈ liminf (highEvent d) atTop at hx34      rw [mem_liminf_iff_eventually_mem] at hx35      apply tendsto_const_nhds.congr'36      filter_upwards [hx] with r hr37      simp [hr]38  simpa only [integral_indicator_const _ (measurableSet_highEvent d _),39    integral_const, measureReal_def, measure_univ, ENNReal.toReal_one,40    smul_eq_mul, mul_one] using hlim4142theorem tendsto_constant_resolvent_highEvent (d : ℕ) (t : PositiveTime) :43    Tendsto (fun r => (resolventMeasure constantRates t).real (highEvent d r))44      atTop (𝓝 1) := by45  let := isProbabilityMeasure_resolventMeasure constantRates t.property46  exact tendsto_probability_highEvent_of_commonSet _ d (constant_resolvent_commonSet t d)4748theorem exists_constant_highEvent (d : ℕ) (t : PositiveTime) {δ : ℝ} (hδ : 0 < δ) :49    ∃ r : ℕ, haar.real (highEvent d r) < δ ∧50      1 - δ < (resolventMeasure constantRates t).real (highEvent d r) := by51  have hhaar := (tendsto_haar_highEvent d).eventually (gt_mem_nhds hδ)52  have hres := (tendsto_constant_resolvent_highEvent d t).eventually53    (lt_mem_nhds (by linarith : 1 - δ < (1 : ℝ)))54  exact (hhaar.and hres).exists5556theorem exists_constant_finite_tail_event (d : ℕ) (t : PositiveTime)57    {δ : ℝ} (hδ : 0 < δ) :58    ∃ (S : Finset ℕ) (B : Set Walsh.Group),59      Disjoint S (Finset.range d) ∧ MeasurableSet B ∧ DependsOn S B ∧60      haar.real B < δ ∧ 1 - δ < (resolventMeasure constantRates t).real B := by61  obtain ⟨r, hh, hr⟩ := exists_constant_highEvent d t hδ62  exact ⟨support d r, highEvent d r, support_disjoint_prefix d r,63    measurableSet_highEvent d r, highEvent_dependsOn d r, hh, hr⟩6465end PL1.TailSpikeEvents6667namespace PL1.TailSpikes68open Noise6970theorem exists_constant_family (d : ℕ) (t : PositiveTime) {δ : ℝ} (hδ : 0 < δ) :71    Nonempty (RateFamily constantRates d t δ) :=72  exists_rateFamily_of_event constantRates d t δ73    (TailSpikeEvents.exists_constant_finite_tail_event d t hδ)7475end PL1.TailSpikes76