PL1/TailSpikes.lean

All source files · Download exact source

SHA-256: b8ad4a7301477a50a99e842d8ea3d0950f771660db1f722f007378b925a50ef8

1import PL1.KernelTranslations2import PL1.TailSpikeEvents34/-!5# Actual finite tail-spike families67This is the paper's tail-spike lemma on the original Haar sign group. The8functions and sets depend only on a displayed finite set of coordinates past9the prescribed prefix; they are the pullbacks of the corresponding tail data.10All averages are finite, and the displayed noise operator is the actual one.11-/1213noncomputable section14open MeasureTheory15open scoped ENNReal NNReal BigOperators1617namespace PL1.TailSpikes18open Walsh Noise FiniteCoordinateKernels1920structure RateFamily (rates : ℕ → ℝ≥0) (d : ℕ) (t : PositiveTime) (δ : ℝ) where21  coordinates : Finset ℕ22  beyond_prefix : Disjoint coordinates (Finset.range d)23  q : Assignments coordinates → C(Walsh.Group, ℝ)24  B : Assignments coordinates → Set Walsh.Group25  q_depends : ∀ a x y, (∀ j ∈ coordinates, x j = y j) → q a x = q a y26  B_depends : ∀ a, DependsOn coordinates (B a)27  nonnegative : ∀ a x, 0 ≤ q a x28  integral_one : ∀ a, ∫ x, q a x ∂haar = 129  measurable : ∀ a, MeasurableSet (B a)30  small : ∀ a, haar.real (B a) < δ31  concentrated : ∀ a, 1 - δ < ∫ x in B a, q a x ∂haar32  average_one : ∀ x, (Fintype.card (Assignments coordinates) : ℝ)⁻¹ * ∑ a, q a x = 133  almost_invariant : ∀ a (u : ℝ≥0),34    ‖noiseL1 ℝ rates u (ContinuousMap.toLp 1 haar ℝ (q a)) -35      ContinuousMap.toLp 1 haar ℝ (q a)‖ ≤ 2 * (1 - Real.exp (-(u : ℝ) / (t : ℝ)))3637abbrev Family (d : ℕ) (t : PositiveTime) (δ : ℝ) := RateFamily schurRates d t δ3839/-- Finite-coordinate concentration events give the full translated family. -/40theorem exists_rateFamily_of_event (rates : ℕ → ℝ≥0) (d : ℕ) (t : PositiveTime) (δ : ℝ)41    (hEvent : ∃ (S : Finset ℕ) (B : Set Walsh.Group),42      Disjoint S (Finset.range d) ∧ MeasurableSet B ∧ DependsOn S B ∧43      haar.real B < δ ∧ 1 - δ < (resolventMeasure rates t).real B) :44    Nonempty (RateFamily rates d t δ) := by45  let := isProbabilityMeasure_resolventMeasure rates t.property46  obtain ⟨S, B, hSd, hBm, hBS, hBsmall, hBmass⟩ :=47    hEvent48  refine ⟨{49    coordinates := S50    beyond_prefix := hSd51    q := fun a => translatedDensity (resolventMeasure rates t) S (extend S a)52    B := fun a => translatedSet B (extend S a)53    q_depends := fun a _ _ hxy => translatedDensity_congr _ S (extend S a) hxy54    B_depends := fun a => dependsOn_translatedSet S hBS (extend S a)55    nonnegative := fun a => translatedDensity_nonneg _ S (extend S a)56    integral_one := fun a => integral_translatedDensity _ S (extend S a)57    measurable := fun a => measurableSet_translatedSet hBm (extend S a)58    small := ?_59    concentrated := ?_60    average_one := average_translatedDensity _ S61    almost_invariant := fun a u => norm_noise_translatedResolventDensity_sub_le rates t S (extend S a) u62  }⟩63  · intro a64    simpa only [measureReal_def, measure_translatedSet hBm] using hBsmall65  · intro a66    rw [setIntegral_translatedDensity _ S hBm hBS]67    exact hBmass6869/-- The complete finite tail-spike construction, with no unproved concentration70or smoothing premises. Positivity of δ is sufficient for the construction. -/71theorem exists_family (d : ℕ) (t : PositiveTime) {δ : ℝ} (hδ : 0 < δ) :72    Nonempty (Family d t δ) :=73  exists_rateFamily_of_event schurRates d t δ (TailSpikeEvents.exists_finite_tail_event d t hδ)7475theorem RateFamily.almost_invariant_time {rates : ℕ → ℝ≥0} {d : ℕ} {t : PositiveTime} {δ : ℝ}76    (Q : RateFamily rates d t δ) (a : Assignments Q.coordinates) (u : ℝ≥0) :77    ‖noiseL1 ℝ rates u (ContinuousMap.toLp 1 haar ℝ (Q.q a)) -78      ContinuousMap.toLp 1 haar ℝ (Q.q a)‖ ≤ 2 * (u : ℝ) / (t : ℝ) :=79  (Q.almost_invariant a u).trans (by80    have h := one_sub_exp_neg_div_le t u81    convert mul_le_mul_of_nonneg_left h (by norm_num : (0 : ℝ) ≤ 2) using 182    ring)8384end PL1.TailSpikes85