PL1/TailSpikeEvents.lean

All source files · Download exact source

SHA-256: 7fb833dcafa347f1d175ebad59b8f5dd6327875137dc5ef4c39233c4f532441a

1import PL1.FiniteCoordinateKernels2import PL1.SingularResolvents34/-!5# Finite tail events with small Haar mass and large resolvent mass67The events are the actual coordinate-average events used in the singular-carrier8proof. Their finite supports avoid any prescribed initial segment. Their Haar9probabilities tend to zero, while every positive-time Schur resolvent assigns10probabilities tending to one.11-/1213noncomputable section14open MeasureTheory Filter15open scoped Topology ENNReal1617namespace PL1.TailSpikeEvents18open Walsh Carrier CarrierAsymptotics Noise FiniteCoordinateKernels1920/-- The coordinates genuinely used by the dyadic average after deleting `d`. -/21def support (d r : ℕ) : Finset ℕ := (Finset.range (2 ^ r)).image (d + ·)2223theorem support_disjoint_prefix (d r : ℕ) :24    Disjoint (support d r) (Finset.range d) := by25  classical26  apply Finset.disjoint_left.mpr27  intro j hj hjd28  obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hj29  have := Finset.mem_range.mp hjd30  omega3132theorem highEvent_dependsOn (d r : ℕ) : DependsOn (support d r) (highEvent d r) := by33  classical34  intro x y hxy35  have havg : Carrier.average d r x = Carrier.average d r y := by36    unfold Carrier.average37    congr 138    apply Finset.sum_congr rfl39    intro j hj40    exact congrArg signValue (hxy (d + j) (Finset.mem_image.mpr ⟨j, hj, rfl⟩))41  simp only [highEvent, Set.mem_ofPred_eq, havg]4243theorem tendsto_haar_highEvent (d : ℕ) :44    Tendsto (fun r => haar.real (highEvent d r)) atTop (𝓝 0) := by45  apply squeeze_zero (fun _ => measureReal_nonneg) _46    summable_haar_failure_bound.tendsto_atTop_zero47  intro r48  have h := ENNReal.toReal_mono (by finiteness) (haar_highEvent_le d r)49  simpa only [measureReal_def, ENNReal.toReal_ofReal (by positivity :50    0 ≤ (1 / 2 : ℝ) ^ r / (threshold r) ^ 2)] using h5152theorem tendsto_schur_resolvent_highEvent (d : ℕ) (t : PositiveTime) :53    Tendsto (fun r => (resolventMeasure schurRates t).real (highEvent d r))54      atTop (𝓝 1) := by55  let := isProbabilityMeasure_resolventMeasure schurRates t.property56  have hae : ∀ᵐ x ∂resolventMeasure schurRates t, x ∈ commonSet d :=57    (mem_ae_iff_prob_eq_one (measurableSet_commonSet d)).mpr58      (schur_resolvent_commonSet t d)59  have hlim : Tendsto (fun r => ∫ x, (highEvent d r).indicator (fun _ => (1 : ℝ)) x60      ∂resolventMeasure schurRates t)61      atTop (𝓝 (∫ _x, (1 : ℝ) ∂resolventMeasure schurRates t)) := by62    apply tendsto_integral_of_dominated_convergence (fun _ => (1 : ℝ))63    · intro r64      exact (measurable_const.indicator (measurableSet_highEvent d r)).aestronglyMeasurable65    · exact integrable_const 166    · intro r67      exact ae_of_all _ (fun x => by68        by_cases hx : x ∈ highEvent d r <;> simp [hx])69    · filter_upwards [hae] with x hx70      change x ∈ liminf (highEvent d) atTop at hx71      rw [mem_liminf_iff_eventually_mem] at hx72      apply tendsto_const_nhds.congr'73      filter_upwards [hx] with r hr74      simp [hr]75  simpa only [integral_indicator_const _ (measurableSet_highEvent d _),76    integral_const, measureReal_def, measure_univ, ENNReal.toReal_one,77    smul_eq_mul, mul_one] using hlim7879/-- One actual finite tail event simultaneously has the two requested masses. -/80theorem exists_highEvent (d : ℕ) (t : PositiveTime) {δ : ℝ} (hδ : 0 < δ) :81    ∃ r : ℕ, haar.real (highEvent d r) < δ ∧82      1 - δ < (resolventMeasure schurRates t).real (highEvent d r) := by83  have hhaar := (tendsto_haar_highEvent d).eventually (gt_mem_nhds hδ)84  have hres := (tendsto_schur_resolvent_highEvent d t).eventually85    (lt_mem_nhds (by linarith : 1 - δ < (1 : ℝ)))86  exact (hhaar.and hres).exists8788theorem exists_finite_tail_event (d : ℕ) (t : PositiveTime) {δ : ℝ} (hδ : 0 < δ) :89    ∃ (S : Finset ℕ) (B : Set Walsh.Group),90      Disjoint S (Finset.range d) ∧ MeasurableSet B ∧ DependsOn S B ∧91      haar.real B < δ ∧ 1 - δ < (resolventMeasure schurRates t).real B := by92  obtain ⟨r, hh, hr⟩ := exists_highEvent d t hδ93  exact ⟨support d r, highEvent d r, support_disjoint_prefix d r,94    measurableSet_highEvent d r, highEvent_dependsOn d r, hh, hr⟩9596end PL1.TailSpikeEvents97