UnionDirectionNet #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The finite direction net of the Section 3.5 response #
This module supplies such a reduction against this repository's carrier: on one
probability-one event, simultaneously for every cutoff scale and every unit
direction, the Section 3.5 response Observable.cutoffResponseJ is at most 2 ^ d times the sum of its values at the d coordinate directions, hence at
most 2 ^ d * d times one of them.
The response is a nonnegative quadratic form in the direction: quadratic
homogeneity and the parallelogram identity are Chapter 2 theorems of
CoarseGraining about responseJ (responseJ_smul, responseJ_parallelogram),
and nonnegativity is another (responseJ_nonneg). No convexity A, no
convexity predicate, no bilinear form and no convex hull is constructed. The
net used here is the d coordinate directions and the cost is 2 ^ d, a
constant depending only on d; the source's own net is the 2 ^ d sign vectors
at cost d. Both are admissible for a source node whose constant scope is
C(d), and the coordinate net is the one for which the decomposition e = sum_i e_i E_i with sum_i e_i ^ 2 = 1 is available directly.
Two deliberate deviations from the source are recorded here. First, the net is the
d coordinate directions rather than the 2 ^ d sign vectors. Second, the
dimensional cost is 2 ^ d (or 2 ^ d * d in the existential form) rather
than the printed d; the sharper printed constant comes from a genuine convexity
argument over the l^infinity box, while the route taken here uses only the
parallelogram identity through R(x + y) <= 2 R(x) + 2 R(y). Both costs
depend on d alone, which is the constant scope recorded for the source node.
The extra factor is absorbed in two places, both inside the printed budget
k = k1 + k2 <= C(d) |log epsilon|: on the two fluctuation lanes by enlarging
the separation k2 (see exists_gridDecay_mul_le in
Provider/Homogenization/UnionAggregation.lean; the increment is
2 log(2 ^ d * d) / (d log 3), bounded in d), and on the deterministic mean
by running the finite-corridor iteration at epsilon / (2 ^ d * d), which
costs k1 an additive C(d). Enlarging k2 alone does not suffice: the
direction net multiplies the mean term as well.
Only one null set is spent: everything below is filter_upwards on the single
statement Observable.ae_forall_coefficientScale_cutoffResponseJ_eq_literal,
whose quantifiers over cutoff scales and loads already sit inside the event.
The uncountable direction quantifier likewise stays inside the event, so no
intersection over directions is taken.
Standing data: M : ABKModel d (through which 0 < d is read off
M.shellPrefix.dimension, never bound). Typing data: d, cubeScale, e,
and the section carriers U, a, sigma of the deterministic lemmas.
The scalar response as a function of the direction alone, with both loads normalized by one positive comparator. This is the object ABK26 maximizes over the unit sphere.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Each coordinate direction is an admissible direction for the Section 3.5 family, that is, a Euclidean unit vector.
On one probability-one event, and simultaneously for every cutoff scale and every direction, the measurable Section 3.5 response is the Chapter 2 response of CoarseGraining at the two normalized loads. This is the form in which the Chapter 2 quadraticity theorems apply to it.
The finite direction net. On one probability-one event, and
simultaneously for every cutoff scale and every Euclidean unit direction, the
Section 3.5 response is bounded by 2 ^ d times the sum of its values at the
d coordinate directions.
The proof uses only the Chapter 2 quadraticity theorems of CoarseGraining --- exact quadratic homogeneity, the parallelogram identity, and nonnegativity --- and the decomposition of a unit vector into coordinates with squared coefficients summing to one. The uncountable direction quantifier sits inside the event, so no intersection over directions is taken.
The consumer form of the direction net: every unit direction is dominated,
on the same event, by one member of the d-element coordinate family, at the
dimensional cost 2 ^ d * d.
This is the shape the aggregation consumes: an existential over a finite index whose quantifier sits inside the almost-sure event.