HomogenizationInput #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the per-cube homogenization input of p.multiscale.estimate #
The proof of ABK26's Proposition p.multiscale.estimate reduces, through
l.localization.mathcalE, to three displays. The first of them is
e.what.homogenization.gives,
s * sum_{l = -infty}^{m} 3^{-s(m-l)}
( avsum_{z in 3^l Z^d cap cu_m}
max_{|e| = 1} J(z + cu_l, shom_{l-h}^{-1/2} e, shom_{l-h}^{1/2} e; a_{l-h})^{d/s}
)^{s/d}
<= O_{Gamma_1}(C s^{-1} eps E^2 cgamma) + O_{Gamma_{1/4}}(C eps exp(-E^{-3} cgamma^{-1})) ,
and the manuscript proves it in one sentence: "an immediate consequence of
Proposition p.homogenization.step, the triangle inequality
e.Gamma.sigma.triangle and the fact that s >= 8 cgamma, provided that h:= C |log eps| for C large enough".
This module is the per-cube half of that sentence: for one scale l
and one grid point z it applies the
Algsuperdiff.Frozen.Section3.homogenization_step at cube scale l and at
eps' := eps^2, and it moves the conclusion from the origin cube cu_l, the
only cube the Section 3 observable reads, to the translated cube z + cu_l
that the localization display carries.
- the
l-sum, theavsum_zvolume average and the twoGamma_sigmatriangle aggregations that turn the per-cube bounds into the display above;
The eps^2 route (development decision D2) #
Two consequences are visible in this module.
- The lanes are the printed ones, a fortiori. At
eps' = eps^2the root emitsO_{Gamma_1}(eps^2 E^2 cgamma) + O_{Gamma_{1/4}}(eps^2 exp(-2 E^{-3} cgamma^{-1})). Sinceeps <= 1/2, both amplitudes are below the printedeps-linear ones, so the printed display is obtained with a surplus half power ofepsin hand. - The
s <= Cms * epswitness clause of the frozenmultiscale_estimatebecomes free. That surplus is exactly what the buckle's square root turns into the refinedGamma_2amplitude:sqrt (eps^2 E^2 cgamma) = eps E sqrt cgamma, which is the clause's own amplitude atCms = 1,s = 1, and therefore belowCms eps E s^{-1} sqrt cgammafor everys <= 1--- nos <= Cms * epsguard is used anywhere.
The Gamma-lane structure #
Both lanes are emitted exactly as the frozen root emits them: the typical
lane at Gamma_1 and the rare lane at Gamma_{1/4}. No index is lowered and
no lane is weakened anywhere below. This matters downstream: records that the
multiscale buckle's rare budget is pinned at Gamma_{1/4} by this very
display and that the Orlicz index can only ever be lowered, so an index loss
introduced here would be unrecoverable.
The translation seam #
Observable.cutoffResponseJ M l L e reads the origin cube cu_l only ---
there is no translate parameter in the observable --- while the localization
display carries z + cu_l on both sides. The bridge is the proved unit-D
transport Provider/Localization/ResponseTransport.lean, whose almost-sure
endpoint identifies the demanded Book.Ch02.responseJ at an arbitrary
descendant R = z + cu_l with the observable read at the translated sample
translateCutoffSample (triadicCubeShift R) omega. Two things are added here
and nothing else:
- section 5, the transport of a common-event two-term bound along that same
translation (the proved translation layer carries the one-term
IsBigOWithand the two-termIsTwoTermBigOWithcases, not the common-event one, whose almost-sure domination clause has to be pulled back along the measure-preserving translation); - section 8, the passage from the root's unit directions
|e| = 1--- the quantifier of the printed display --- to the loading ball|v|^2 <= 2in whichProvider/Localization/Breakdown.leanandResponseTransport's consumption interface state the two breakdown legs. This is the quadratic homogeneity ofJ, at the price of the factor2that the ball costs; it is a deterministic identity and commits to no amplitude.
No gap was found in the transport lane: every identity this module needed was
either already public there or is the CoarseGraining quadraticity theorem
Book.Ch02.responseJ_smul.
References #
- ABK26,
e.what.homogenization.gives, and its proof sentence. - ABK26,
p.homogenization.step(the frozenhomogenization_step). - ABK26,
e.mathcal.E.breakdown(the legs atz + cu_l).
1. The homogenization constant #
The homogenization constant of the p.homogenization.step: the existential
witness of Algsuperdiff.Frozen.Section3.homogenization_step, which depends on
the dimension alone.
Instances For
The homogenization constant is at least one, by the frozen statement.
The homogenization constant is positive.
The homogenization step, at the named constant. This is the frozen
homogenization_step with its existential witness replaced by
homogenizationStepConst d; it is a restatement, binder for binder, and proves
nothing new. Every later declaration in this file goes through it, so the
frozen root is applied exactly once.
2. The eps^2 substitution #
The root's own window premise and its corridor are the only two places where
eps' occurs syntactically, and both survive the substitution eps' := eps^2
free of charge: the window because eps <= 1/2 forces eps^2 <= 1/4, and the
corridor because |log (eps^2)| = 2 |log eps|, which is the cost
h |-> 2 Chom |log eps| that decision D2 records.
3. The preceding-error premise at a lower cube scale #
The root's third premise is verbatim the second conjunct of the frozen
inductionState, at m0 := m - 1. Applying the root at a cube scale l <= m
asks for it at l - 1, which is a restriction of the same clause; no premise
is added and none is strengthened.
Premise inheritance. The preceding-error clause the root demands at cube
scale l is the second conjunct of the induction state inductionState M m0 E
whenever l - 1 <= m0 --- in particular at m0 = m - 1 for every l <= m,
which is the situation of p.multiscale.estimate's own binder.
4. The per-cube input at the origin cube #
The per-cube homogenization input, at the origin cube of scale l. The
p.homogenization.step applied at cube scale l and at eps' := eps^2: one
pair of measurable envelopes dominates, on one event of probability one,
the response J(cu_l, sigmaBar_L^{-1/2} e, sigmaBar_L^{1/2} e; a_L)
simultaneously for every coefficient-cutoff scale L in the corridor L <= l - 2 Chom |log eps| and every unit direction e, at the two amplitudes
Gamma_1 : eps^2 E^2 cgamma ,
Gamma_{1/4} : eps^2 exp(-2 E^{-3} cgamma^{-1}) .
Both are the frozen root's own amplitudes at eps' = eps^2; both lanes carry
the frozen root's own Orlicz indices. Since eps <= 1/2, both are below the
eps-linear amplitudes the display e.what.homogenization.gives prints, so the
printed lanes follow a fortiori and the surplus half power of eps is the one
decision D2 spends on the Gamma_2 refinement.
5. Translation of a common-event two-term bound #
The common-event carrier is translation invariant. A two-term weak-Orlicz bound with one common domination event for an indexed family of observables of the cutoff sample holds verbatim --- same envelopes up to the translation, same Orlicz profiles, same amplitudes --- for the family read at every real translate of the sample.
The two tail lanes are moved by the proved
Stream.isBigOWith_comp_translateCutoffSample; the only new step is the common
domination event, which is pulled back along the measure-preserving
translation, so the index quantifier stays inside one event and no intersection
over the index is taken. The single probabilistic input is the J1
stationarity of the model, consumed as the fact
map_translateCutoffSample_cutoffSampleLaw and never as a hypothesis.
6. The per-cube input at the translated cube #
The per-cube homogenization input, transported. The statement of
isCommonEventTwoTermBigOWith_cutoffResponseJ_epsSq for the observable read at
the translated sample. Instantiated at z := triadicCubeShift R this is the
input at the grid cube R = z + cu_l, which is the carrier the localization
display uses; the translation is the Lean carrier device forced by the fact that
Observable.cutoffResponseJ reads the origin cube only, and it changes neither
amplitude nor Orlicz index.
7. The literal per-(l, z) response of the printed display #
The homogenization input at the printed carrier. For a grid cube
R = z + cu_l of the printed tiling 3^l Z^d cap cu_m, one pair of measurable
envelopes with the two frozen tails dominates, on one event of probability one,
the manuscript's own quantity
J(z + cu_l, sigmaBar_L^{-1/2} e, sigmaBar_L^{1/2} e; a_L)
simultaneously for every coefficient-cutoff scale L in the corridor and every
unit direction e. This is e.what.homogenization.gives before the avsum_z
average and the l-sum, at eps' := eps^2.
The envelopes are stated as an explicit ∃ Y Z rather than through
IsCommonEventTwoTermBigOWith on purpose: the literal Book.Ch02.responseJ of
the cutoff family is not known to be measurable --- that is exactly why
Section 3 carries the measurable representative Observable.cutoffResponseJ
--- so the common-event carrier, which demands measurability of every member,
is not available at this spelling. The almost-sure identification of the two
spellings is the proved unit-D endpoint, consumed here.
That concession is about the family, not about the envelopes: Measurable Y
and Measurable Z are carried as the first two conjuncts of the conclusion,
because Y and Z are existentially bound here and could not be recovered by
any consumer afterwards, while every consumer needs them --- the frozen
IsTwoTermBigOWithWitnesses demands Measurable Y and Measurable Z
(Section3/Probability/TwoTermOrlicz.lean), and so does every proved
Gamma_sigma triangle engine that this display exists to feed
(Provider/Orlicz/TwoTermCalculus.lean, Provider/Orlicz/TsumTriangle.lean).
They cost nothing: they are two of the fields of the common-event datum this
proof already destructures.
The form of exists_envelope_responseJ_descendant_epsSq whose premises are
literally the binders of the frozen multiscale_estimate: the preceding-error
clause is supplied by that theorem's own induction state
inductionState M (m-1) E, restricted from m - 1 to l - 1.
8. From unit directions to the loading ball of the localization legs #
The printed display and the frozen root quantify over unit directions |e| = 1;
Provider/Localization/Breakdown.lean and ResponseTransport's consumption
interface state the two breakdown legs over the loading ball |v|^2 <= 2, the
frame vectors e_1 -+ e_2 of the paired families. The passage between the two
is the quadratic homogeneity of J, at the price of the factor 2 the ball
costs. Both lemmas are deterministic: no measure, no amplitude and no Orlicz
datum appears.
Quadratic homogeneity of the response in the loading direction. The two
comparator loads are linear in the direction, so J is quadratic in it.
The seam to the localization legs. A bound on the response over the
unit sphere --- the quantifier of e.what.homogenization.gives and of the frozen
homogenization step --- bounds it over the loading ball |v|^2 <= 2 of the
breakdown legs, at the cost of the factor 2.
The per-cube bound is the hypothesis of the statement, not a premise of the module: nothing here asserts that such a bound holds.