PrincipalResponseBudgetDescent #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.
Provider: the deterministic leg of the budget of e.use.also.for.the.upper.bound #
This module supplies the two deterministic inequalities of the chain printed in ABK26, namely the passage
bfJ(cu_n, bfAhom^{-1/2} e, bfAhom^{1/2} e; a)
<= mathcalE_{s,infinity,2}(cu_n; a, a_0)^2
<= 3^{2 s (N - n)} mathcalE_{s,infinity,2}(cu_N; a, a_0)^2 ,
for an arbitrary triadic coefficient family a, at the isotropic comparator
a_0 = sigma Id, on the tower of centered cubes cu_n subset cu_N. The first
step is the first inequality of e.mathcalE.monotone.ordered, squared; the
second is e.bound.one.cube.by.mathcalE, in its per-descendant form, also
squared.
Everything below is pointwise in the coefficient field: no law, no expectation,
no induction state. The probabilistic half of the budget is the second moment
of mathcalE, which is not touched here.
The probe #
What is proved first is that this pair is literally an element of
CoarseGraining's normalized block-response value set
Ch02.normalizedBlockResponseValueSet of the comparator
Observable.isotropicComparatorMatrix sigma, whose doubled unit witness is
Sum.elim e_1 e_2; that is exactly the sense in which mathcalE maximizes
over the same probe family. The manuscript's normalization |e| = 1 is the
hypothesis hE : blockVecDot = 1, which
...PrincipalResponseSwitch.exists_blockVecDot_self_eq_one shows is
satisfiable.
The exponent #
The third line of the manuscript's chain carries the factor 3^{t(m-h-n)} in
front of the second moment of mathcalE. Composing the first inequality of
e.mathcalE.monotone.ordered (which squares) with
e.bound.one.cube.by.mathcalE (stated for mathcalE itself) produces 3^{2 t (m-h-n)}, not 3^{t(m-h-n)}. Under the manuscript's own scale choice both
factors are absolute constants, so nothing downstream moves.
Main results #
doubledResponseJ_annealedProbe_mem_normalizedBlockResponseValueSet: the tex probe is a probe ofmathcalE.doubledResponseJ_annealedProbe_le_sq_homogenizationErrorOnCube: the first inequality ofe.mathcalE.monotone.ordered, squared, at that probe.homogenizationErrorOnCube_originCube_le_rpow_mul:e.bound.one.cube.by.mathcalEon the centered tower.
References #
- ABK26,
e.mathcalE.monotone.ordered. - ABK26,
e.bound.one.cube.by.mathcalE. - ABK26,
e.use.also.for.the.upper.bound(statement, proof, and thealign*chain).
Real-power bookkeeping #
ABK26 against d.mathcal.E. The pair
(bfAhom^{-1/2} e, bfAhom^{1/2} e) at the isotropic comparator sigma Id
realizes the doubled response bfJ as an element of the normalized
block-response value set whose supremum mathcalE maximizes. The doubled
witness is Sum.elim e_1 e_2, whose squared Euclidean norm is the manuscript's
|e|^2.
The first inequality of e.mathcalE.monotone.ordered, squared #
ABK26, first inequality, squared, at the annealed probe. The doubled
response of a cube at the probe (bfAhom^{-1/2} e, bfAhom^{1/2} e) is at most
the square of mathcalE_{s,infinity,2} of that cube.
e.bound.one.cube.by.mathcalE on the centered tower #
ABK26, per-descendant form, on the centered cubes.
For n <= N,
mathcalE_{s,infinity,2}(cu_n) <= 3^{s(N-n)} mathcalE_{s,infinity,2}(cu_N).
The deterministic leg #
The deterministic leg of the budget of ABK26.
At the annealed probe of ABK26, on the centered tower cu_n subset cu_N,
bfJ(cu_n, bfAhom^{-1/2} e, bfAhom^{1/2} e; a)
<= 3^{2 s (N-n)} mathcalE_{s,infinity,2}(cu_N; a, sigma Id)^2 .
No law and no induction state occur; the remaining half of the manuscript's chain is the second moment of the right-hand side.