Step5SampDefMeasurable #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Sample measurability of the Step-5 per-cube cross defect #
ABK26, l.approximate.recurrence.formula, Step 5, e.nablaw.oscillations.
The obligation this module discharges #
Closure.Step5InputSideConditions records that the one remaining binder of
Closure.Step5Input.closureStep5Input_of_sampDef --- the sample integrability of
Closure.JunctionDischargeStepFiveDisplay.step5CrossDefect at the closure's
Dirichlet family --- is missing exactly one ingredient: the sample measurability
of the cube average of a product,
omega |-> fint_R e . ( (k_m - k_n)(x) grad w_D(omega)(x) ) dx .
The two factors are separately measurable, but the corrector gradient enters
every proved statement only through its L^2 class, never through a jointly
measurable representative, so the product's cube average is not a composition
of proved maps. This module supplies it.
Method: the pairing is a Caratheodory function of the class #
The cube average above is a bilinear pairing. Written against the
transposed direction (k_m - k_n)^t e and localized to the cube by an
indicator, it is the L^2(cu_K) inner product
fint_R e . (h(x) v(x)) dx = (cubeVolume R)^{-1} < W(omega) , [v] > ,
W(omega) := 1_{cu_R} (h(omega, .)^t e) ,
so that, at fixed sample, it is a continuous function of the L^2 class
[v] (it is a fixed continuous linear functional), while at fixed class it is
a measurable function of the sample (the weight is jointly (omega, x)
measurable --- the shell field's evaluation map is jointly continuous --- so
MeasureTheory.StronglyMeasurable.integral_prod_right' applies).
MeasureTheory.measurable_uncurry_of_continuous_of_measurable (Caratheodory)
then makes the two-variable pairing jointly measurable, and composing with the
proved measurable gradient class
Corrector.measurable_freshShellDirichletGradL2 finishes.
This is the same route the joint-measurability lane uses for the doubled energy
value in ApproximateRecurrence.LocalizationFluctuationJointField; only the
functional changes (a linear pairing here, a quadratic form there).
No measurable selection occurs. The corrector family is an arbitrary family
of weak solutions of e.def.w, exactly as in
Corrector.CorrectorMeasurableGradient, and only its gradient class is read.
Because the pairing depends on the gradient only through its class, its value at
the class is equal --- not merely almost surely equal --- to the cube average
of the honest representative.
Main results #
measurable_uncurry_finiteShellIncrement_entry--- joint(omega, x)measurability of the entries ofk_m - k_n.step5CrossPairing,continuous_step5CrossPairing,step5CrossPairing_apply_class--- the localized pairing, its continuity in the class, and its value at the class of anyL^2field.measurable_step5CrossPairing_apply--- measurability in the sample at a fixed class.measurable_cubeAverage_vecDot_matVecMul_freshShellDirichletGrad--- the missing ingredient itself.measurable_step5CrossDefect_freshShellDirichletGradand its cutoff-sample corollary --- sample measurability of the whole per-cube cross defect.
Binders #
Beyond the typing binders: [NeZero d] (for the proved gradient-class
measurability) and the zero-trace weak-solution property of e.def.w for the
corrector family. No integrability, no estimate, no smallness and no
measurability of the corrector family itself is assumed.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formula, Step 5;e.nablaw.oscillations;e.def.w.
Joint (omega, x) measurability of the finite shell increment #
The evaluation map of the frozen shell carrier is jointly continuous: the carrier is a subtype of a compact-open triple whose first component is a bundled continuous map.
One shell coordinate of a sequence, jointly measurable in (omega, x).
Joint (omega, x) measurability of the entries of k_m - k_n. The
increment is the finite sum of the shells with indices in (n, m].
The transposed direction #
The direction e pushed through the transpose of a matrix.
Equations
- Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.step5CrossWeightVec e A j = ∑ i : Fin d, e i * A i j
Instances For
Testing a matrix-vector product against e is testing the vector against
the transposed direction.
The localized weight field #
The Step-5 weight: the transposed direction against the fresh shell,
localized to the cube R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The weight is bounded --- the fresh shell is continuous, hence bounded on the
closed cube --- so it is L^2 on any localization cube.
The pairing #
Restricting the localization cube's measure to a descendant is the descendant's own restricted measure: the two differ only inside a null boundary.
The Step-5 cross pairing: the normalized L^2(cu_K) pairing of the
localized weight with a class.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At a fixed sample the pairing is a continuous function of the class: it is a fixed continuous linear functional.
The pairing computes the cube average of the product. No integrability of the product is assumed: both sides are Bochner integrals of almost everywhere equal integrands against the same measure.
At a fixed class the pairing is a measurable function of the sample: the
integrand is jointly (omega, x) measurable.
The Caratheodory composition #
The missing ingredient of hsampDef, proved.
The cube average of the product of the fresh shell and the Dirichlet corrector's gradient, tested against a fixed direction, is a measurable function of the sample.
only on the zero-trace weak-solution property of e.def.w: the corrector
family is otherwise arbitrary, and no measurable selection occurs.
The defect itself #
Sample measurability of the Step-5 per-cube cross defect. The cube average of the product is the previous statement; the product of the two averages is the proved pair of measurable factors.
The cutoff-sample carrier form of the previous statement.