Finite second moments of cycle occupations

Ordered pairs of visits reduce level second moments to the killed-gap Green kernel. Finite bands are finite sums of level counts; stopped restart transfers square integrability from the first cycle to every cycle.

theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_levelOccupation_sq_add_le (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {y : ℕ} (hy : 0 < y) : ∫⁻ (ω : ℕ → ℕ), levelOccupation y ω ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ) + 1 ≤ 2 * killedGapGreen μ y y

The positive-level occupation second moment plus its mean is at most twice the killed Green diagonal.

theorem BGW.StableTrees.DiscreteHeightApprox.levelOccupation_zero_eq_one (ω : ℕ → ℕ) : levelOccupation 0 ω = 1

The zero-gap occupation consists of the time-zero visit alone, on every sequence.

theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_levelOccupation_sq_lt_top (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (y : ℕ) : ∫⁻ (ω : ℕ → ℕ), levelOccupation y ω ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ) < ⊤

Every integer-level occupation has a finite second moment, without a variance assumption.

theorem BGW.StableTrees.DiscreteHeightApprox.integrable_clusterLevel_sq (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (y : ℕ) : MeasureTheory.Integrable (fun (ω : ℕ → ℕ) => ↑{u ∈ Finset.Ico 0 (weakEpoch ω 1) | reflGap ω u = ↑y}.card ^ 2) ↑(DiscreteForest.offspringSeqLaw μ)

The square of a first-cycle integer-level count is integrable.

theorem BGW.StableTrees.DiscreteHeightApprox.integrable_clusterVisits_sq (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {a : ℝ} (ha : 0 < a) (i : ℕ) : MeasureTheory.Integrable (fun (ω : ℕ → ℕ) => ↑(clusterVisits ω a i) ^ 2) ↑(DiscreteForest.offspringSeqLaw μ)

Square-integrability supplier (Sol audit finding 1). Lean's Bochner integral is totalized to 0 off integrable functions, so finite second moments are supplied explicitly. Proof: finite killed-walk Green entries and ordered pairs of level visits.

theorem BGW.StableTrees.DiscreteHeightApprox.integral_clusterLevel_sq_add_one_le (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {y : ℕ} (hy : 0 < y) : ∫ (ω : ℕ → ℕ), ↑{u ∈ Finset.Ico 0 (weakEpoch ω 1) | reflGap ω u = ↑y}.card ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ) + 1 ≤ 2 * (killedGapGreen μ y y).toReal

The real exact-level second moment plus its mean is at most twice the Green diagonal.