LocalizationFluctuationSelectEndpoint #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-2 endpoint integrand: well-posed, de-existentialized, consumer-shaped #
ABK26, l.approximate.recurrence.formula, Steps 1--2, read at the recurrence
pair (n, n+h) of the closure junctions.
What this module does #
The proved structural split
LocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded
holds one sample at a time and delivers the two cell fields S_z, tilde S_z through an existential. The Step-3 consumer
Closure.AnnealedLimitJunction.annealedSplitEndpoint_of_integral_ch02CoarseBlockMatrix_le
needs the sample integral of that split's left-hand side, so its right-hand
side has to be an honest function of the sample. Three things are supplied
here.
De-existentialization (
blockVecDot_recurrenceP_le_descendantsAverage_switch_add_fluctuation). The split's right-hand side is rewritten, at each cell, asswitchCubeEnergyplus the canonical numberLocalizationFluctuationSelectValue.localizationFluctuationValue, which is a function of the cell datum only. The existential quantifiers vanish from the statement: no minimizer is chosen, and no measurable selection of the minimizer family is needed, because the two printed fluctuation summands only ever enter through their sum, and that sum is a difference of two variational minima. See theLocalizationFluctuationSelectValueheader for why this is the form the no-choice-without-uniqueness rule demands: the field-slope minimizer is unique only a.e., so a chosen witness would carry no information, while the number is choice-free.The interchange (
integral_descendantsAverage,integrable_descendantsAverage,descendantsAverage_add).descendantsAverageis a normalized sum over the finiteFinsetdescendantsAtDepth (cu_{Kc}) j, so the sample integral passes through it as soon as each cell integrand is sample-integrable. Both directions are proved, with the per-cell integrability as an explicit binder.The carrier identification (
switchCubeEnergy_eq_blockVecDot_coarseBlockMatrix,principalPz_shell_normalize,localizationFz_shell_normalize). The principal summand of the split is the Chapter 2 coarse pairingP_z. bfA(z+cu_n) P_z, andswitchCubeEnergyis by definition that pairing (PrincipalResponseSwitchActualPerCube.switchCubeEnergy); the identification therefore already exists in the cone and isrfl. The only genuinely missing piece was the shell-index normalization(n + h) - h = nbetween the split's(m, h)indexing and the junctions'(n, n+h)indexing; it is proved here. The neighbouring identification of the annealed layer's cube matrix with the Chapter 2 one is the provedClosure.AnnealedLimitPassage.coarseBlockMatrix_cubeSet_coefficientCutoff_eq_ch02and is not restated.
The endpoint #
integral_blockVecDot_recurrenceP_le_principalSwitchEnergyAverage_add packages
1--3: it produces
E[ P . bfA_{n+h}(cu_{Kc}) P ]
<= principalSwitchEnergyAverage + fluctuationEnergyAverage ,
whose first summand is, verbatim, Closure.Junctions.principalEnergyAverage M n h Kc j e e' wD wN with its definition unfolded (that module is a live lane
and is deliberately not imported here; the two terms are syntactically equal
after unfold). A fold lane that proves
fluctuationEnergyAverage M n h Kc j e e' wD wN <= M.gamma ^ 10
--- which is Step 2, --- therefore closes the hypothesis hfinite of
annealedSplitEndpoint_of_integral_ch02CoarseBlockMatrix_le by one le_trans.
That composition was checked, in an untracked probe that additionally
imports Closure.AnnealedLimitJunction (not imported here: Closure is a live
lane). Both halves elaborate:
example ... : principalSwitchEnergyAverage M n h Kc j e e' wD wN
= Closure.principalEnergyAverage M n h Kc j e e' wD wN := rfl
example ... (hstep2 : fluctuationEnergyAverage M n h Kc j e e' wD wN
<= M.gamma ^ (10 : Nat)) :
Closure.AnnealedSplitEndpoint M n h Kc j e e' wD wN :=
Closure.annealedSplitEndpoint_of_integral_ch02CoarseBlockMatrix_le M n h Kc j Kc
e e' wD wN
(le_trans
(integral_blockVecDot_recurrenceP_le_principalSwitchEnergyAverage_add M n Kc h
hK e e' j hscale wD wN hwD hwN hintLHS hintPrincipal hintFluctuation)
(by ... linarith))
The junction is instantiated at the cube scale K := Kc, i.e. at the same
large cube the split localizes inside; no second scale is introduced.
The surviving obligations, stated exactly #
The endpoint carries three integrability binders and no other analytic hypothesis:
hintLHS--- sample-integrability of the coarse quadratic form oncu_{Kc};hintPrincipal--- sample-integrability ofswitchCubeEnergyatP_z, per cell. A producer of the a.e.-strong measurability half is proved (PrincipalResponseGoodEnergy.aestronglyMeasurable_switchCubeEnergy, which consumes a measurableP_zfamily); the domination half is the good-event/bad-event budget of Step 3.hintFluctuation--- sample-integrability of the canonical fluctuation number, per cell. The fluctuation number is instead a variational minimum in which the sample enters through both the coefficienta_omegaand the slope fieldbfF_z(omega), and no proved statement asserts thatomega |-> mu_field(U, a_omega; F_omega)is measurable. The exact missing statement is recorded in the docstring offluctuationEnergyAverage.
References #
descendantsAverage is a finite normalized sum #
Two cell functions that agree on the grid have the same descendant average.
The descendant average is additive.
The interchange of the sample integral with the cell average #
Sample integrability of the cell average from per-cell integrability.
The grid is a Finset, so this is a finite sum of integrable functions.
The interchange int_omega avsum_z = avsum_z int_omega. The cell
average is a normalized finite sum, so the sample integral passes through it as
soon as every cell integrand is sample-integrable. This is item (b) of the
gamma^{10} endpoint chain.
The de-existentialized split at the recurrence pair #
The localized variational test, with the existential removed (at the
recurrence pair (n, n+h)).
P . bfA_{n+h}(cu_{Kc}) P
<= avsum_z ( switchCubeEnergy(P_z) + fluct(z+cu_n; P_z, bfF_z) ) ,
with P = recurrenceP (shom_n) e e' and fluct the canonical fluctuation
number of LocalizationFluctuationSelectValue. The right-hand side mentions
no minimizer: it is a function of the sample, the two correctors and the
geometry only, so it can be integrated in the sample without any selection.
exactly on the binders of the proved split it is derived from --- the
large-cube gate, the depth-naming identity, and the two weak formulations of
e.def.w. No measurability, integrability or smallness proposition occurs.
The endpoint carriers #
The per-cell Step-2 integrand. The canonical fluctuation number at the
recurrence carriers, as a function of the sample. Both correctors are read
along the sample, exactly as Closure.Junctions.principalEnergyAverage reads
them.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The principal half of the endpoint, at the terminal's carrier. This is
A compatibility name for the lower shared principalEnergyAverage carrier.
The closure and localization consumer lanes both import that carrier directly.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The fluctuation half of the endpoint: the quantity Step 2 must bound by
cgamma^{10} (target e.lower.bound.localization.terms).
The missing producer, stated exactly, is sample-integrability of the cell
integrand: for each R in descendantsAtDepth (cu_{Kc}) j,
Integrable (fun omega => meshFluctuationCellIntegrand M n h Kc e e' wD wN R omega)
((cutoffSampleLaw M).toMeasure) .
The proved measurability statements
(Provider.Diffusivity.Corrector.CorrectorMeasurable{Forcing,Gradient,Consumer, Quartic}, and LocalizationFluctuationCellIntegrable.measurable_volumeAverage_ vecNormSq_freshShell{Dirichlet,Neumann}Grad) all factor through continuous or
Borel functionals of the L^2 class of grad w_omega at a fixed coefficient.
omega |-> doubledMuField (cubeDomain R) (a_omega) (F_omega)
in either argument. Producing it is a separate, self-contained task.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The endpoint #
The Step-1/2 endpoint, well-posed and consumer-shaped.
E[ P . bfA_{n+h}(cu_{Kc}) P ]
<= principalSwitchEnergyAverage + fluctuationEnergyAverage .
The left-hand side is verbatim the left-hand side of the hypothesis hfinite
of Closure.AnnealedLimitJunction.annealedSplitEndpoint_of_integral_ch02CoarseBlockMatrix_le
at K := Kc, and the first summand on the right is verbatim
Closure.Junctions.principalEnergyAverage M n h Kc j e e' wD wN unfolded. A
fold lane that proves fluctuationEnergyAverage <= M.gamma ^ 10 therefore
closes Junction 3 with le_trans and add_le_add_left.
No estimate on anything is assumed.