LeanPool.AsymptoticTrianglePacking.Internal — the tight round with CONCRETE parameters #
LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round (in
LeanPool.AsymptoticTrianglePacking.Internal.Tight.TightRound) is stated with abstract moment
bounds
Vb, Pb and an abstract coverage rate qlo. Here those abstract data are instantiated in terms
of the hypergraph parameters only:
r— the uniformity,Δ— a global degree ceiling,δ— a global degree floor,κ— a codegree ceiling,p— the retention probability.
The resulting statement LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_of_params
is the tight nibble round in the form
in which the iteration consumes it: one round, one outcome, a two-sided band around the SAME centre
for all but a vertices, and a guaranteed coverage fraction.
placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].
Concrete moment bounds #
The uniform pair bound: two vertices are simultaneously covered with probability at most
Δ²p² + κp.
The variance of the loss weight in terms of the hypergraph parameters.
The mean of the pair count in terms of the hypergraph parameters.
The tight round with concrete parameters #
The tight nibble round, concrete form.
For an r-uniform hypergraph whose degrees lie in [δ, Δ] and whose codegrees are at most κ,
one Bernoulli round with retention probability p admits an outcome which
- covers more than a
qlo/2-fraction of the vertex set, whereqlo = δ·p·(1−p)^{rΔ}, and - leaves every vertex outside an exceptional set of size
< awith its safe degree inside the two-sided banddeg(v) − 𝔼[loss(v)] ± (t, t+s).
All the moment data are explicit functions of r, Δ, κ, p; the only requirement is the smallness
condition hsmall, which in the nibble regime p = γ/Δ is satisfied for t ≍ ξ γ Δ,
s ≍ ξ γ Δ and a = θ·|V| once γ is small.
LeanPool.AsymptoticTrianglePacking.Internal — one round preserves a TIGHT degree band on the #
residual
LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_of_params produces, for one
Bernoulli round, an outcome whose SAFE
degrees sit in a two-sided band around deg(v) − 𝔼[loss(v)]. Here that is converted into the form
the iteration needs: a bound on the DEGREES OF THE RESIDUAL HYPERGRAPH, valid for every uncovered
vertex outside a small exceptional set, with the band expressed purely in the parameters
r, Δ, δ, κ, p.
The two ingredients are
LeanPool.AsymptoticTrianglePacking.Internal.lossWeightMean_le/LeanPool.AsymptoticTrianglePacking.Internal.lossWeightMean_ge— the mean loss is squeezed between(r−1)·δ·q_loand(r−1)·Δ·q_hi, so the centre of the band is itself pinned down; andLeanPool.AsymptoticTrianglePacking.Internal.safeDegree_eq_residual_degree_of_not_covered— on the event thatvsurvives the round, its safe degree IS its residual degree.
The resulting band has width (Δ − δ) + ((r−1)Δq_hi − (r−1)δq_lo) + 2t + s. In the nibble regime
p = γ/Δ, Δ ≤ (1+μ)δ with μ, γ → 0 this is (1 + o(1)) times the new mean degree — i.e. the
round MAINTAINS near-regularity, which is exactly what the refuted wide-band (U/L ≤ 8) peeling
cannot do.
placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].
Squeezing the mean loss #
The mean loss is at most (r−1)·deg(v)·q_hi.
The mean loss is at least (r−1)·deg(v)·q_lo.
The residual band #
One round maintains a tight degree band.
For an r-uniform hypergraph with degrees in [δ, Δ] and codegrees ≤ κ, there is a retained
subfamily R' ⊆ H (an outcome of the Bernoulli round) and an exceptional set B of size < a
such that every vertex that is left uncovered and lies outside B has its degree in the RESIDUAL
hypergraph inside the explicit band
δ − (r−1)Δq_hi − t ≤ deg_res(v) ≤ Δ − (r−1)δq_lo + t + s,
with q_hi = Δp and q_lo = δp(1−p)^{rΔ}; moreover the round covers more than a q_lo/2-fraction
of the vertex set.
LeanPool.AsymptoticTrianglePacking.Internal — the tight round with a CHEBYSHEV coverage guarantee #
LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_on extracts a good outcome by
making two failure probabilities add up to
less than one:
- "too many bad vertices", controlled by Markov, probability
≤ N(Vb/t² + Pb/s)/a; - "too little coverage", controlled by Markov applied to the UNCOVERED count, probability
≤ 1 − q/2.
Because the second bound is only 1 − q/2, the first has to be < q/2 ≈ γ/2; with a = θN this
forces Vb/t² + Pb/s ≤ θγ, hence (since Pb ≈ Δγ²) s ≳ γΔ/θ. A band of width ≍ γΔ cannot be
iterated: over the ≍ γ^{-1}log(1/β) rounds of a nibble it accumulates to a relative error
≍ log(1/β)/θ ≫ 1.
Here the coverage is instead controlled by CHEBYSHEV, using the variance bound
LeanPool.AsymptoticTrianglePacking.Internal.coveredCount_variance_le. The coverage failure
probability becomes 4·Var/Q², which is
≤ 1/2 under hypotheses on the vertex count and the codegree ALONE. The badness budget is then a
constant rather than γ, so Vb/t² + Pb/s ≤ θ/2 suffices and one may take
s ≍ Δγ²/θ and t ≍ γ²Δ,
i.e. deviations of relative size γ², whose accumulation over γ^{-1}log(1/β) rounds is
≍ γ·log(1/β) → 0. This is the form of the round the iteration needs.
placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].
The deterministic band. If the loss weight of v is within t of its mean and the pair
count of v is below s, then the safe degree of v lies in the two-sided band of width 2t + s
around deg(v) − 𝔼[loss(v)].
The tight round with Chebyshev coverage.
There is an outcome of the nibble round which
- leaves fewer than
avertices outside the two-sided safe-degree band of width2t + sarounddeg(v) − 𝔼[loss(v)], and - covers more than
Q/2vertices,
provided the Markov badness bound N(Vb/t² + Pb/s)/a and the Chebyshev coverage bound
Cvar/(Q/2)² add up to less than 1.
Compared with LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_on, the coverage
failure probability is Cvar/(Q/2)²
instead of 1 − q/2: the badness budget is a constant instead of O(q).
LeanPool.AsymptoticTrianglePacking.Internal — the Chebyshev tight round in explicit hypergraph #
parameters
This file instantiates LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_cheb with
the codegree-tightened moment data of
LeanPool.AsymptoticTrianglePacking.Internal.Tight.PairExcessCodegree and converts it into the form
the iteration consumes: a bound on
the DEGREES OF THE RESIDUAL hypergraph for every uncovered vertex outside a small exceptional set,
together with a coverage guarantee.
Writing N = |V|, q_lo = δ·p(1−p)^{rΔ}, q_hi = Δp and
ε₂ = κp + 4r²κΔ²p³,
Vb = κ(r−1)Δ·Δp + ε₂·((r−1)Δ)²,
Pb = Δ(r−1)²(Δ²p² + κp),
Cvar = N·q_hi + N²·ε₂,
the single hypothesis is
N(Vb/t² + Pb/s)/a + Cvar/(N q_lo/2)² < 1.
In the nibble regime p = γ/((r−1)Δ), κ = μΔ, Δ ≍ δ ≍ d, a = θN, t = s = γ²d:
Vb ≈ C_r μγ d², soN·Vb/t²/a = Vb/(θ t²) ≈ C_r μ/(θγ³);Pb ≈ C_r γ² d, soN·Pb/s/a = Pb/(θ s) ≈ C_r/(θ d);Cvar/(N q_lo/2)² ≈ 4/(N γ) + 4 C_r μ/γ.
All four terms are < 1/4 once μ ≤ c(r)θγ³, d ≥ d₀(r, θ) and N ≥ 16/γ — and the tolerances
t = s = γ²d are SECOND order in γ, hence summable over the ≍ γ^{-1}log(1/β) rounds of a
nibble. This is exactly what the Markov-coverage round
LeanPool.AsymptoticTrianglePacking.Internal.exists_round_residual_band cannot
provide (there s ≳ γd/θ, first order in γ).
placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].
The Chebyshev tight round in explicit parameters. For an r-uniform hypergraph with
degrees in [δ, Δ] and codegrees ≤ κ, one Bernoulli round with retention probability p has an
outcome covering more than N·q_lo/2 vertices and leaving all but < a vertices with a safe degree
in the band deg(v) − 𝔼[loss(v)] ± (t, t+s).
One Chebyshev round maintains a tight degree band on the residual.
Every vertex left uncovered and outside an exceptional set of size < a has its residual degree in
the band
δ − (r−1)Δq_hi − t ≤ deg_res(v) ≤ Δ − (r−1)δq_lo + t + s,
and the round covers more than N·q_lo/2 vertices.
LeanPool.AsymptoticTrianglePacking.Internal — existence of a Bernoulli retention space #
Standalone, Mathlib-only. The measure-theoretic prerequisite for the nibble iteration (step 2):
for any finite hypergraph H on a finite vertex type and any retention probability p ∈ [0,1],
there EXISTS a probability space carrying a BernoulliRetention on H at p — an independent
family of events A e (e retained) each of probability p.
Standard construction: Ω := Finset V → Bool (finite, since V is a Fintype) with the product
Bernoulli(p) measure Measure.pi (fun _ => (Bernoulli) p); A e := {ω | ω e = true}. The
coordinate events are independent (product measure) and each has probability p.
Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].
Existence of a Bernoulli retention. For any finite hypergraph H on a finite vertex type
and any p ∈ [0,1], there is a probability space carrying a BernoulliRetention on H at p.
LeanPool.AsymptoticTrianglePacking.Internal — a nibble round with FULLY EXPLICIT parameters #
LeanPool.AsymptoticTrianglePacking.Internal.exists_round_residual_band_cheb produces a good round
outcome under one smallness
hypothesis relating the tolerances t, s, the exceptional budget a and the moment data. Here
that hypothesis is DISCHARGED for a concrete parameter choice, giving an unconditional round.
For a round parameter γ ∈ (0, 1/2] and an exceptional fraction θ ∈ (0,1] put
p = γ/(rΔ), t = γ²Δ, s = 16γ²Δ/θ, a = θN.
If the hypergraph is r-uniform (r ≥ 2) with degrees in [δ, Δ], 1 ≤ δ, Δ ≤ 2δ, codegrees at
most κ ≤ θγ³Δ/(1280 r) and N = |V| ≥ 512r/γ, then the Markov badness bound and the Chebyshev
coverage bound add up to at most 3/4 (cheb_smallness_explicit), so one round leaves all but
< θN of the surviving vertices with residual degree in
[δ − γΔ − γ²Δ, Δ − (r−1)δγ/(4r) + γ²Δ + 16γ²Δ/θ]
while covering more than Nγ/(8r) vertices (exists_round_explicit).
The point is that BOTH tolerances are of second order in γ (γ²Δ, up to the constant 16/θ),
whereas the first-order drop is ≍ γΔ. That is what makes the round iterable: over the
≍ γ^{-1}log(1/β) rounds of a nibble the tolerances accumulate to ≍ γ·log(1/β)/θ → 0, while with
the Markov-coverage round (LeanPool.AsymptoticTrianglePacking.Internal.exists_round_residual_band)
the tolerance s is necessarily
first order in γ and the accumulation does not vanish.
placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].
The arithmetic core #
All the estimates below are inequalities between real numbers; R is the uniformity, D the
degree ceiling, dd the degree floor, k the codegree ceiling, N the number of vertices and
L = (1−p)^{rΔ} the conflict factor of the covering rate.
The smallness condition of the Chebyshev round holds for the explicit parameter choice.
The Markov badness bound is at most 1/4 and the Chebyshev coverage bound at most 1/2.
The round #
A nibble round with explicit parameters.
For r ≥ 2, γ ∈ (0,1/2], θ ∈ (0,1], an r-uniform hypergraph with degrees in [δ, Δ],
1 ≤ δ, Δ ≤ 2δ, codegrees ≤ κ ≤ θγ³Δ/(1280r) and |V| ≥ 512r/γ, there is a retained subfamily
R' ⊆ H and an exceptional set B of fewer than θ|V| vertices such that
Iterable tight-band round #
This module establishes the one-round estimates used by the finite near-regular hypergraph nibble. It packages retention, concentration, degree-band, codegree, and cover-rate bounds in a form that can be iterated by the schedule.
The iterable (sharp) nibble round.
For uniformity r ≥ 2 and free parameters
γ— the round rate (retentionp = γ/(rΔ)),ε— the relative tolerance: both band tolerances areε·γΔ, a factorεbelow the first-order per-round gain≍ γΔ,θ— the exceptional fraction: at mostθ|V|vertices leave the band,α— the guaranteed relative size of the live setA,
there are a degree threshold D₀ and a codegree factor c₀ such that every r-uniform hypergraph
K with
- a GLOBAL degree ceiling
Δ, - a degree floor
δon the live setA, withΔ ≤ 2δ, - codegrees at most
κ ≤ c₀Δ, Δ ≥ D₀,|V| ≥ D₀and|A| ≥ α|V|,
admits a retained set R' ⊆ K and an exceptional set B, |B| ≤ θ|V|, such that
- every live, uncovered
v ∉ Bhas residual degree at leastδ − ((r−1)/r)γΔ − εγΔand at mostΔ − ((r−1)/r)·γ·(δ − lost(v))·δ·(1−γ)/Δ + εγΔ, wherelost(v) = lostDegree K Aᶜ vcounts the edges atvleavingA, and - the round covers at least a
γ/(8r)fraction ofA.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The iterable (sharp) nibble round, packaged: for every uniformity and every choice of the
four free parameters there are a degree threshold D₀ and a codegree factor c₀ for which
LeanPool.AsymptoticTrianglePacking.Internal.SharpRoundFor holds.
Equations
- One or more equations did not get rendered due to their size.