A criterion for Assumption (S): Lemma lem:critM

Source lines 1051–1110 (Lemma 3.4 and its proof), 264–268 (the remark that E_{k_n}[C_{k_n} + L_{k_n}] = n^{o(1)} suffices), inventory L3.4.

For η ∈ (0, 1 - 1/α) the cutoff is M_n = max 1 ⌊n^(1-η)⌋₊; it equals the paper's ⌊n^(1-η)⌋ for every n ≥ 1, and the max 1 only repairs n = 0 so that IsCutoff holds (correction F11 of docs/BRIDGE_PLAN.md).

• isCutoff_max_one_floor_rpow: M_n is a cutoff sequence (M_n ≥ 1, M_n → ∞, M_n = o(n)) for η ∈ (0, 1).
• measureReal_lt_le_div: Markov's inequality P(C > x) ≤ E[C] / x for the core size of a decomposition (any measure, finite first moment).
• critM (Lemma lem:critM): given the decompositions ρ_k of Assumption (S) (only required at marks of positive probability, as in StructuralMicroscopic) with E_{k_n}[C_{k_n} + L_{k_n}] ≤ n^δ eventually along admissible sizes for every δ > 0, Assumption (S) holds with respect to M_n. The proof is the paper's: Markov's inequality and the regular-variation limits tendsto_mul_div_floor_rpow, tendsto_div_floor_rpow.

The hypothesis E_{k_n}[C + L] = n^{o(1)} is used only through its upper half E_{k_n}[C + L] ≤ n^{o(1)}, and only along admissible sizes; this is how it is stated.

theorem PoissonDeclumping.Bridge.isCutoff_max_one_floor_rpow {η : ℝ} (h0 : 0 < η) (h1 : η < 1) : IsCutoff fun (n : ℕ) => max 1 ⌊↑n ^ (1 - η)⌋₊

The polynomial cutoff M_n = max 1 ⌊n^(1-η)⌋₊ (= ⌊n^(1-η)⌋ for n ≥ 1) is a cutoff sequence for η ∈ (0, 1): M_n ≥ 1, M_n → ∞ and M_n = o(n) (source line 233).

theorem PoissonDeclumping.Bridge.measureReal_lt_le_div (ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)) {x : ℝ} (hx : 0 < x) (hfin : ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑ω.2.1 ∂ρ ≠ ⊤) : ρ.real {ω : PlaneTree × ℕ × List PlaneTree | x < ↑ω.2.1} ≤ (∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑ω.2.1 ∂ρ).toReal / x

Markov's inequality for the core size C of a decomposition (source line 1093): P(C > x) ≤ E[C] / x for x > 0, for any measure with E[C] < ∞.

theorem PoissonDeclumping.Bridge.critM {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {η : ℝ} (hη : 0 < η ∧ η < 1 - 1 / α) {G : ℕ → PlaneTree → Prop} {k : ℕ → ℕ} (ρ : ℕ → MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)) (hρ : ∀ (j : ℕ), 0 < (PlaneTree.bienayme μ) {T : PlaneTree | G j T} → Skeleton μ (G j) (ρ j)) (hmom : ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in admissibleSizes μ, ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑ω.2.1 + ↑ω.2.2.length ∂ρ (k n) ≤ ENNReal.ofReal (↑n ^ δ)) : StructuralMicroscopic μ a G k fun (n : ℕ) => max 1 ⌊↑n ^ (1 - η)⌋₊

Lemma lem:critM (source lines 1055–1109). Let ρ_j be decompositions as in Assumption (S) (Skeleton, required at every mark of positive probability) with E_{k_n}[C_{k_n} + L_{k_n}] = n^{o(1)}, used in the form: for every δ > 0, eventually along admissible sizes, E_{k_n}[C_{k_n} + L_{k_n}] ≤ n^δ. Then for every η ∈ (0, 1 - 1/α) Assumption (S) holds along (k_n) with respect to M_n = max 1 ⌊n^(1-η)⌋₊ (which is ⌊n^(1-η)⌋ for n ≥ 1), with the same decompositions ρ.