ClosureFinalMeasurability #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The two typing binders of the closure's energy display #

ABK26, e.perturb.assumption read at the corrector families Closure.closureDirichletFamily and Closure.closureNeumannFamily chosen by Closure.ClosureAssembly.

ClosureAssembly reduces the drift limit hlimit of both assembly skeletons to the two AEStronglyMeasurable binders hDm, hNm that the proved display Corrector.ShellSumEnergyDisplay.tendsto_integral_cutoffSample_cubeAverage_display carries, and records that they are "not built here". This module builds them.

The chain #

The two families are Classical.choose selections, so nothing about their dependence on the path f is available from the construction. What is available is the same fact that Corrector.CorrectorMeasurableGradient uses for the sample carrier: the gradient of a weak solution is not merely some chosen element, it is the value at the forcing class of the fixed continuous solution operator of Corrector.MeasurablePrereqSolutionOperator. Three steps:

closureForcingL2_eq_contMatrixFieldL2 --- the forcing class of the closure families is Corrector.contMatrixFieldL2 at the direction (-c) • e; the realization of valuePathForcing at a path is the literal matrix-vector product, so the two L^2 classes are the class of one and the same function.
continuous_gradToHilbertVectorL2_closureDirichletFamily and its Neumann mirror --- composing Corrector.continuous_contMatrixFieldL2 with Corrector.continuous_dirichletGradientOfForcingClass (resp. the Neumann operator) gives continuity of f |-> grad w(f) in the L^2 carrier.
cubeAverage_vecDot_grad_eq_norm_sq --- the cube energy is the squared L^2 norm of that class, normalized by the cube volume, so it is a continuous, hence Borel measurable, hence AEStronglyMeasurable function of the path.

What is supplied #

aestronglyMeasurable_cubeAverage_closureDirichletFamily, aestronglyMeasurable_cubeAverage_closureNeumannFamily --- the binders hDm and hNm of Closure.tendsto_dirichletCubeEnergy_closureDirichletFamily, Closure.tendsto_neumannCubeEnergy_closureNeumannFamily and the two conditional assemblies, verbatim. Discharging them there is what makes those drift limits unconditional in the corrector data.

References #

ABK26, e.def.w; e.perturb.assumption.
ABK26 (the fresh-shell measurability parenthetical).

The forcing class of the closure families #

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureForcingL2_eq_contMatrixFieldL2 {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (e : HCPolySupport.Vec d) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) :

HCPolySupport.toHilbertVectorL2OfVecField ⋯ = Corrector.contMatrixFieldL2 Q (-c • e) f

The forcing class of the closure's corrector families is the continuous matrix-field class of Corrector.CorrectorMeasurableForcing, at the direction (-c) • e.

The realization of valuePathForcing (c • e) at a continuous path f is the literal matrix-vector product f(x) (c • e), so the two L^2 classes are the class of one and the same function; only the membership witnesses differ, and the class does not depend on those.

Continuity of the two gradient classes in the path #

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.continuous_gradToHilbertVectorL2_closureDirichletFamily {d : ℕ} [NeZero d] (c : ℝ) (e : HCPolySupport.Vec d) (K : ℕ) :

Continuous fun (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => (closureDirichletFamily c e K f).gradToHilbertVectorL2

The Dirichlet corrector gradient of the closure family is a continuous function of the increment path.

No property of the Classical.choose selection is used: the gradient class of any zero-trace weak solution is the value of the continuous Dirichlet solution operator at the forcing class.

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.continuous_gradToHilbertVectorL2_closureNeumannFamily {d : ℕ} (c : ℝ) (e : HCPolySupport.Vec d) (K : ℕ) :

Continuous fun (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => (closureNeumannFamily c e K f).gradToHilbertVectorL2

The Neumann corrector gradient of the closure family is a continuous function of the increment path. The mean-zero mirror of the previous statement.

The cube energy as a continuous functional of the gradient class #

source

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeAverage_vecDot_grad_eq_norm_sq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) :

(HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (u.grad x) (u.grad x)) = (HCPolySupport.cubeVolume Q)⁻¹ * ‖u.gradToHilbertVectorL2‖ ^ 2

The cube average of |grad w|^2 is the squared L^2 norm of the gradient class, normalized by the cube volume. The cube boundary is Lebesgue null, so the closed-cube average of cubeAverage and the open-cube L^2 norm of the class agree.

source