KickFamily #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-1 annular kick family of l.minimal.scale.sep #
ABK26, §4.2, Step 1 of l.minimal.scale.sep. The manuscript's Step 1 opens
with the inner-scale sum
Σ_{i ≤ j−1} 3^{−½s(j−i)} max_{z ∈ 3^i ℤ^d ∩ (□_j ∖ □_{j−1})}
𝓔_{s,2,2}(z + □_i; 𝐚_{i−2}, σ_{i−2})
This module builds the sum — the unsquared sibling of the §4.1 𝒢₂ object
Proportion.errorAnnMax, at the §4.2 weight 3^{−½s·} rather than 3^{−¼s·}
— together with the two legs X_j^{(1)}, X_j^{(2)}, their locality, and their
r-dependence.
The leg construction, and why it is a clamp #
X_j^{(1)} and X_j^{(2)} are the clamp and the overshoot of the sum at
a deterministic threshold lam:
X_j^{(1)} = min(annularKick_j, lam) , X_j^{(2)} = annularKick_j − min(annularKick_j, lam) ,
X_j^{(1)} + X_j^{(2)} = annularKick_j exactly.
Both legs are therefore measurable functions of the single variable
annularKick_j, and that is the point: the manuscript's Step 1 claims that
X_j^{(i)} and X_{j'}^{(i')} are independent for |j − j'| > 1, for each
i, i' ∈ {1,2} — a joint statement about the pair. Any leg decomposition
built from the two Γ-witnesses of the induction bound would fail it: those
witnesses are supplied by the Section 3 anchor as bare existentials and carry
no locality whatsoever. With the clamp, the joint claim is a one-line
push-forward of the r-dependence of annularKick, which is itself a one-line
consequence of the proved bridge Section4.Probability.rDependent_of_annulusLocalSigma.
The threshold that makes the two clamped legs carry the manuscript's Γ₂ and
Γ_{1/2} amplitudes is chosen in KickTails.lean; nothing in this file
depends on its value, so lam is a free real parameter throughout.
Main definitions #
kickAtom— the per-cube atom𝓔_{s,2,2}(z + □_i; 𝐚_{i−2}, σ_{i−2}), rendered by translating the sample (resolution A4) at the public measurable(2,2)observable, unsquared.kickAnnMax— the0-floored lattice-annulus maximum of the atom.annularKickE/annularKick— the weighted inner-scale sum, formed inℝ≥0∞and read back intoℝ.kickLegLow/kickLegHigh— the two legsX_j^{(1)}, X_j^{(2)}.
Main results #
annularKickE_eq_wsumE,annularKick_eq_wsum— the bridge to theℕ-indexed weighted-series apparatus ofProportion.SeriesTail, so the tail machinery is reused verbatim.measurable_annularKick_annulusRegion_local— locality at truncation levelj − 2onannulusRegion d j, thehXslot of ther-dependence bridge.
Deviations from the printed text #
- (inherited from §4.1) — the summand reads the field at the inner scale
i; this is the provedSupport.annularErrorObservableat indexi, so the convention is the manuscript's. - (inherited) — the
(2,2)observable is the measurable representative, choice-dependent on a null set; every statement below is a statement about that same representative, and the locality step absorbs the choice throughProportion.measurable_cutoffSampleLocalSigma_of_ae_eq. - The leg split is a construction, not a printed definition: exhibits no
X_j^{(i)}. See the module note above for why the clamp is the reading that supports the printed independence claim.
References #
- ABK26,
l.minimal.scale.sep, Step 1.
1. The unsquared per-cube atom #
The Step-1 per-cube atom 𝓔_{s,2,2}(z + □_i; 𝐚_{i−2}, σ_{i−2}),
rendered by translating the sample (resolution A4) at the public measurable
(2,2) observable. This is Proportion.errorAtomSq without the square: §4.2
Step 1 never squares.
Equations
Instances For
The atom is the square root of the §4.1 squared atom; this is the one line that
lets the proved 𝒢₂ locality export be reused unmodified.
2. The lattice-annulus maximum #
The lattice-annulus maximum: max_{z ∈ 3^i ℤ^d ∩ (□_j ∖ □_{j−1})} 𝓔_{s,2,2}(z + □_i; 𝐚_{i−2}, σ_{i−2}), 0-floored so that it is total (the
annulus enumeration may be empty).
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The weighted inner-scale sum #
The Step-1 inner-scale sum, formed in ℝ≥0∞: Σ_{i ≤ j−1} 3^{−½s(j−i)} · kickAnnMax_j(i). The weight is the §4.2 weight 3^{−½s·} — half the decay
rate of the §4.1 𝒢₂ lane, because §4.2 Step 1 does not square.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real-valued inner-scale sum; at the sample points where the ℝ≥0∞ sum is
infinite this is 0, which only strengthens every upper-tail statement about
it.
Equations
Instances For
The bridge to the ℕ-indexed weighted-series apparatus. The inner
scales i ≤ j − 1 are enumerated by the offset p = j − 1 − i, at which the
weight is weightThird (½s) (p+1).
4. Locality on the annulus of the own index #
The unsquared atom is local, at truncation level i − 2 and every region
containing the closed cube z + □_i = ⟨i, v⟩. Obtained from the proved 𝒢₂
export Proportion.measurable_errorAtomSq_local by a square root: the atom is
nonnegative, so no information is lost.
The lattice-annulus maximum is local on the annulus region of its own
index: every read cube ⟨i, v⟩ with v in the annulus enumeration sits inside
annulusRegion d j, and every truncation level i − 2 is at or below j − 2.
The Step-1 inner-scale sum is local on annulusRegion d j at truncation
level j − 2 — the hX slot of the r-dependence bridge.
5. r-dependence #
The Step-1 family is r-dependent, for every r ≥ 1 clearing the honest
separation count 3 + 2·3^{1−2}·√d ≤ 3^r of the proved bridge at truncation
offset c = 2.
6. The two legs #
The Γ₂ leg X_j^{(1)}: the inner-scale sum clamped at the deterministic
threshold lam.
Equations
- Algsuperdiff.Section4.Provider.MinimalScale.kickLegLow M s lam j omega = min (Algsuperdiff.Section4.Provider.MinimalScale.annularKick M s j omega) lam
Instances For
The Γ_{1/2} leg X_j^{(2)}: the overshoot of the inner-scale sum above
lam.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The split is exact: X_j^{(1)} + X_j^{(2)} is the inner-scale sum on the
nose, at every sample point. Nothing is dropped and no null set enters.