Two-point sets, integer levels and subsequence splitting

Deterministic bookkeeping behind the two-point and one-point localization statements of Theorems thm:max_string(ii) and thm:max_lh(ii) (source lines 486–501, 2860–2897, 545–558, 3363–3383; inventory P20, P24).

• The two-point set J_n = twoPointSet x ({m-1, m} if θ ≤ 1/2, {m, m+1} otherwise, with m = ⌊x⌋, θ = {x}) is the integer interval [a, a+2) with a = twoPointLow x = ⌈x - 1/2⌉ - 1 (twoPointSet_eq, mem_twoPointSet_iff). In both cases a ≤ x - 1/2 and x + 1/2 ≤ a + 2 (twoPointLow_le, add_half_le_twoPointLow_add_two), so the paper's case split at θ_n = 1/2 can be replaced by one level sequence a_n valid for all n.
• In the interior phase δ ≤ min(θ, 1 - θ): ⌊x⌋ ≤ x - δ and x + δ ≤ ⌊x⌋ + 1.
• Integer levels versus natural mark indices: for H : ℕ and z : ℤ, z ≤ H ↔ z.toNat ≤ H holds for every z (negative floors included), so the events {H ≤ ⌊y⌋}, {H ∈ J} and {H = ⌊x⌋} are expressed through the events {k ≤ H} at the natural levels k = (·).toNat, with no "eventually" needed.
• Subsequence splitting (source lines 2876–2880): a limit along l ⊓ 𝓟 S and along l ⊓ 𝓟 Sᶜ (either possibly trivial) gives the limit along l.

theorem PoissonDeclumping.TwoPointLocalization.tendsto_singlePoint {μ : PMF ℕ} {H : PlaneTree → ℕ} {x : ℕ → ℝ} (h : TwoPointLocalization μ H x) (hphase : ∃ (δ : ℝ), 0 < δ ∧ ∀ᶠ (n : ℕ) in admissibleSizes μ, δ ≤ min (Int.fract (x n)) (1 - Int.fract (x n))) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | ↑(H T) = ⌊x n⌋}) (admissibleSizes μ) (nhds 1)

The strengthened localization contract retains the original full-filter refinement.

theorem PoissonDeclumping.TwoPointLocalization.tendsto_singlePoint_subsequence {μ : PMF ℕ} {H : PlaneTree → ℕ} {x : ℕ → ℝ} (h : TwoPointLocalization μ H x) {s : ℕ → ℕ} (hs : Filter.Tendsto s Filter.atTop Filter.atTop) (hadm : ∀ᶠ (n : ℕ) in Filter.atTop, PlaneTree.Admissible μ (s n)) (hphase : ∃ (δ : ℝ), 0 < δ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, δ ≤ min (Int.fract (x (s n))) (1 - Int.fract (x (s n)))) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ (s n)).real {T : PlaneTree | ↑(H T) = ⌊x (s n)⌋}) Filter.atTop (nhds 1)

Single-point localization along any cofinal admissible subsequence with interior phases.

The two-point set as an integer interval

noncomputable def PoissonDeclumping.ExtremesAnalysis.twoPointLow (x : ℝ) : ℤ

The lower point a = ⌈x - 1/2⌉ - 1 of the two-point set J = {a, a + 1}: it is ⌊x⌋ - 1 if {x} ≤ 1/2 and ⌊x⌋ otherwise.

Equations

• PoissonDeclumping.ExtremesAnalysis.twoPointLow x = ⌈x - 1 / 2⌉ - 1

theorem PoissonDeclumping.ExtremesAnalysis.twoPointLow_eq_of_fract_le {x : ℝ} (h : Int.fract x ≤ 1 / 2) : twoPointLow x = ⌊x⌋ - 1

theorem PoissonDeclumping.ExtremesAnalysis.twoPointLow_eq_of_lt_fract {x : ℝ} (h : 1 / 2 < Int.fract x) : twoPointLow x = ⌊x⌋

theorem PoissonDeclumping.ExtremesAnalysis.twoPointSet_eq (x : ℝ) : twoPointSet x = {twoPointLow x, twoPointLow x + 1}

J = twoPointSet x = {a, a + 1} with a = twoPointLow x.

theorem PoissonDeclumping.ExtremesAnalysis.mem_twoPointSet_iff (x : ℝ) (z : ℤ) : z ∈ twoPointSet x ↔ twoPointLow x ≤ z ∧ z < twoPointLow x + 2

z ∈ J ↔ a ≤ z < a + 2.

theorem PoissonDeclumping.ExtremesAnalysis.twoPointLow_le (x : ℝ) : ↑(twoPointLow x) ≤ x - 1 / 2

a ≤ x - 1/2, i.e. the lower level lies at least 1/2 below the centering.

theorem PoissonDeclumping.ExtremesAnalysis.sub_le_twoPointLow (x : ℝ) : x - 3 / 2 ≤ ↑(twoPointLow x)

x - 3/2 ≤ a.

theorem PoissonDeclumping.ExtremesAnalysis.add_half_le_twoPointLow_add_two (x : ℝ) : x + 1 / 2 ≤ ↑(twoPointLow x + 2)

x + 1/2 ≤ a + 2, i.e. the first excluded level lies at least 1/2 above the centering.

theorem PoissonDeclumping.ExtremesAnalysis.twoPointLow_add_two_le (x : ℝ) : ↑(twoPointLow x + 2) ≤ x + 3 / 2

a + 2 ≤ x + 3/2.

The interior phase

theorem PoissonDeclumping.ExtremesAnalysis.floor_le_sub_of_le_min {x δ : ℝ} (h : δ ≤ min (Int.fract x) (1 - Int.fract x)) : ↑⌊x⌋ ≤ x - δ

Interior phase: if δ ≤ min({x}, 1 - {x}) then ⌊x⌋ ≤ x - δ.

theorem PoissonDeclumping.ExtremesAnalysis.add_le_floor_add_one_of_le_min {x δ : ℝ} (h : δ ≤ min (Int.fract x) (1 - Int.fract x)) : x + δ ≤ ↑(⌊x⌋ + 1)

Interior phase: if δ ≤ min({x}, 1 - {x}) then x + δ ≤ ⌊x⌋ + 1.

theorem PoissonDeclumping.ExtremesAnalysis.floor_sub_eq_floor_of_phase {x δ : ℝ} (hδ : 0 < δ) (h : δ ≤ min (Int.fract x) (1 - Int.fract x)) : ⌊x - δ⌋ = ⌊x⌋

A lower level shifted away from the centering equals the floor in an interior phase.

theorem PoissonDeclumping.ExtremesAnalysis.ceil_add_eq_floor_add_one_of_phase {x δ : ℝ} (hδ : 0 < δ) (h : δ ≤ min (Int.fract x) (1 - Int.fract x)) : ⌈x + δ⌉ = ⌊x⌋ + 1

An upper level shifted away from the centering equals the next integer in an interior phase.

Integer levels and natural mark indices

theorem PoissonDeclumping.ExtremesAnalysis.int_le_natCast_iff_toNat_le (z : ℤ) (H : ℕ) : z ≤ ↑H ↔ z.toNat ≤ H

For every integer z (negative ones included), z ≤ H ↔ z.toNat ≤ H.

theorem PoissonDeclumping.ExtremesAnalysis.natCast_le_iff_not_toNat_le (H : ℕ) (m : ℤ) : ↑H ≤ m ↔ ¬(m + 1).toNat ≤ H

{H ≤ m} = {(m+1).toNat ≤ H}ᶜ, for every integer m (used with m = ⌊x_n + t⌋).

theorem PoissonDeclumping.ExtremesAnalysis.natCast_mem_twoPointSet_iff (x : ℝ) (H : ℕ) : ↑H ∈ twoPointSet x ↔ (twoPointLow x).toNat ≤ H ∧ ¬(twoPointLow x + 2).toNat ≤ H

{H ∈ J} = {a.toNat ≤ H} \ {(a+2).toNat ≤ H} with a = twoPointLow x.

theorem PoissonDeclumping.ExtremesAnalysis.natCast_eq_iff (H : ℕ) (m : ℤ) : ↑H = m ↔ m.toNat ≤ H ∧ ¬(m + 1).toNat ≤ H

{H = m} = {m.toNat ≤ H} \ {(m+1).toNat ≤ H} for every integer m (used with m = ⌊x_n⌋).

theorem PoissonDeclumping.ExtremesAnalysis.cast_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) : ↑z.toNat = ↑z

If the level z is nonnegative its natural index has the same real value.

theorem PoissonDeclumping.ExtremesAnalysis.eventually_cast_toNat_eq {ι : Type u_1} {l : Filter ι} {x : ι → ℝ} {z : ι → ℤ} {K : ℝ} (hx : Filter.Tendsto x l Filter.atTop) (hz : ∀ᶠ (i : ι) in l, x i - K ≤ ↑(z i)) : ∀ᶠ (i : ι) in l, 0 ≤ z i ∧ ↑(z i).toNat = ↑(z i)

If x_n → ∞ along l and the integer levels z_n satisfy x_n - K ≤ z_n, then the levels are eventually nonnegative, so that (z_n.toNat : ℝ) = z_n eventually.

Subsequence splitting

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_of_tendsto_inf_principal_of_compl {α : Type u_1} {β : Type u_2} {l : Filter α} {l' : Filter β} {f : α → β} (S : Set α) (h₁ : Filter.Tendsto f (l ⊓ Filter.principal S) l') (h₂ : Filter.Tendsto f (l ⊓ Filter.principal Sᶜ) l') : Filter.Tendsto f l l'

Subsequence splitting: a limit along the indices in S and along the indices outside S (either set possibly finite or empty) gives the limit along the whole filter.

theorem PoissonDeclumping.ExtremesAnalysis.tendsto_of_fract_le_half_of_half_lt {α : Type u_1} {β : Type u_2} {l : Filter α} {l' : Filter β} {f : α → β} (x : α → ℝ) (h₁ : Filter.Tendsto f (l ⊓ Filter.principal {n : α | Int.fract (x n) ≤ 1 / 2}) l') (h₂ : Filter.Tendsto f (l ⊓ Filter.principal {n : α | 1 / 2 < Int.fract (x n)}) l') : Filter.Tendsto f l l'

The split used in the source (lines 2876–2880, 3363–3374) for the two-point localization: along the indices with {x_n} ≤ 1/2 and along those with {x_n} > 1/2.