ZAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The witness Z = max{Z¹, Z²}, its measurability, and the conditional endpoint #
ABK26, §4.2. The witness is the random
minimal scale of the disjunction of the two bad-window families, which is
pointwise the maximum of the two legs (Algsuperdiff.Probability.minimalScale).
Three things then come for free, for every omega and with no
measurability side condition:
- both deterministic clauses (
clauses_of_zWitness_le) — strictly stronger than the frozen statement's∀ᵐ; - the tail at the common rate with the two prefactors added
(
measure_tail_zWitness_le).
The conditional endpoint #
frozen_body_of_slots is a conditional endpoint. Its conditional
inputs are exactly
hZ1tail— theZ¹leg's tail: Markov onl.minimal.scale.sep/e.good.scale.kickingplus the same centre union bound,hZ1clause— theZ¹leg's deterministic clause, andhZ1measurable— per-window measurability of theZ¹bad family.
Everything else in the proposition — the Z² leg end to end, the witness, the
measurability, the max tail, and both clauses — is unconditional.
The s-exponent #
Every public here reads the regime clause at s⁹, i.e. the frozen
e.scale.sep.cond with the single numeral 8 replaced by 9. See
ZDensityLeg.lean's module docstring: the centre union bound of the Z² leg
needs γ ≤ K(d)⁻¹ c⋆² s⁹ δ² and the printed clause supplies only s⁸, a gap of
one power of the free parameter s. This is the ONLY deviation from the
printed hypotheses; the tail rate, the tolerance s * Real.sqrt delta, the
window, the centre set and both displays are byte-identical to the frozen
statement.
References #
- ABK26,
p.minimal.scale.separation.sec4.
1. The witness #
The proposition's random scale Z_m(s,δ) = max{Z¹, Z²}, realised as the
random minimal scale of the disjunction of the two bad-window families.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The max assembly, as an identity. The witness is the pointwise maximum of the two legs.
Measurable Z (the survey's empty-sweep-1 clause). It reduces to
per-window measurability of the two bad families; the density leg is proved in
ZScores.lean.
The tail event of the witness is the union of the two legs' tail events.
2. Both deterministic clauses #
The two deterministic halves, together. If the
witness is at most the window length (m − n).toNat, then both frozen displays
hold at the window [n, m]. This holds for every omega: no almost-sure
qualifier, no finiteness, no measurability. The density half is unconditional;
the Cesàro half is exactly hZ1clause.
3. The Z² tail in the additive shape #
The Z² tail at half the prefactor and the un-halved rate — the shape
that adds to a Z¹ tail of the same shape and produces the frozen display at the
single constant C.
Length-0 windows are free (measure ≤ 1 ≤ C/2), and for N ≥ 1 the rate
num/((C/2)γ) delivered by measure_tail_badDensity_le at C/2 dominates the
displayed num/(Cγ).
4. The max tail at the frozen display #
e.scale.sep.bounds, at the frozen prefactor-tail shape. The tail of
max{Z¹, Z²} is the sum of the two legs' tails (tail_set_zWitness plus
subadditivity), so two tails at prefactor C/2 give one at prefactor C, with
the rate untouched.
5. The conditional endpoint #
The conditional endpoint (abstract Z¹ leg). The full body of the
frozen proposition — the witness, its measurability, the prefactor tail and
both a.e. displays — from the proposition's own parameter ranges and window,
the regime clause at s⁹ (see the module docstring for the s⁸ → s⁹
deviation), and exactly three conditional inputs about the Z¹ leg:
hZ1measurable, hZ1tail and hZ1clause.
The Z² leg, the witness, Measurable Z, the max tail and the density display
are all unconditional.
The delivered constant is a single C with 2 · zTwoConst d ≤ C; the frozen
∃ C is obtained by taking C := 2 · max (zTwoConst d) (Wave-D's floor).