LiteralMeasurabilityEngine #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The genuine measurability engine for multiscale ellipticity of a carrier source #
This module is the CoarseGraining-only half of
Provider/BadEvents/LiteralMeasurability.lean, split off as an importable leaf
so that the files owning the Section 3 ellipticity observables
(Observable/CutoffMultiscaleEllipticity.lean,
Provider/BadEvents/CubeEllipticity.lean) can prove genuine measurability of
their own definitions without importing anything above them. The split point
is the section Literals header of the original module; no statement and no
proof below is changed by the split, and every public name is preserved
(namespace Algsuperdiff.Section3.Provider.BadEvents, as before). Nothing
here mentions a Section 3 object.
Given a measurable carrier source X : Omega -> RegCoeffField d that is locally
a.e.-uniformly elliptic at every sample, the two multiscale endpoints
Lambda_{s,q}(Q; X omega) and lambda_{s,q}(Q; X omega)^{-1} are genuinely
measurable, not merely a.e.-measurable.
Why the CoarseGraining a.e. interface does not already give this #
CoarseGraining's public multiscale-ellipticity measurability
(aemeasurable_lambdaSqCoeffField_inv, aemeasurable_LambdaSqCoeffField, and
their Section 3 mirrors in Observable/Ch04MultiscaleMeasurability.lean) is
law-relative for a reason recorded in
Homogenization/Book/Ch04/Theorems/Mu.lean: Mu ∘ toFun is not
LocalSigmaR-measurable on all of the honest carrier, because off the
a.e.-elliptic locus the carrier contains fields on which Mu is uninformative.
Every step above Mu — the coarse blocks, the descendant maxima, the weighted
series, the two endpoints — is then reduced modulo a null set by
filter_upwards [hP.ae_locallyUniformlyEllipticField].
The genuine statement is available all the same, because a composite that never visits the bad locus never needs the null set. So the route taken here is:
exists_localSigmaR_measurable_eq_Mu_cubeSetrebuilds CoarseGraining'sliftCoverassembly and keeps the everywhere-on-the-covered-locus equality thatexists_isLocalRandomVariable_ae_eq_Mu_cubeSetdiscards, giving a genuinelyLocalSigmaR (cubeSet Q)-measurableYwithMu (cubeSet Q) a.toFun = Y aat every field lying in some countable a.e.-elliptic quantitative slice;measurable_comp_Mu_cubeSetcomposes that with any measurable, everywhere locally a.e.-uniformly elliptic carrier sourceX : Omega -> RegCoeffField d;- the
measurable_comp_*chain then re-runs the Section 3 a.e. proof withfilter_upwardsreplaced byfunext omega, since each pointwise identity holds at everyomega.
The Section 3 instantiation X := Cutoff.coefficientCutoff M.nu cutoffScale,
which discharges the two generic hypotheses unconditionally, is made in the
files that own the observables.
Main results #
measurable_comp_coarseB_cubeSet,measurable_comp_coarseSigmaStarInv_cubeSet,measurable_comp_coarseBMatrixNorm,measurable_comp_coarseSigmaStarInvMatrixNorm: the coarse blocks and their operator norms.measurable_comp_maxDescendantB,measurable_comp_maxDescendantSigmaStarInv,measurable_comp_weightedBSeries,measurable_comp_weightedSigmaSeries: the finite descendant maxima and the two weighted series.measurable_comp_LambdaSqCoeffField,measurable_comp_lambdaSqCoeffField_inv(with their finite/infinity halves): the two multiscale endpoints for an arbitrary carrier source.
Related statements elsewhere #
Provider/BadEvents/LambdaLocal.lean already states the pivotal
everywhere-ellipticity dichotomy in its own docstring and carries the analogous
liftCover assembly (a plain ℕ-indexed cover on CutoffSample d; the Option ℕ
cover with its none branch is this file's, on RegCoeffField d) and genuine
measurability of the two general-cube literals at the local σ-algebra
cutoffSampleLocalSigma --- a completion-comap that is incomparable with the
ambient carrier σ-algebra, so nothing here is redundant.
References #
- ABK26, (2.22)--(2.23) (the coarse-grained ellipticity constants).
Homogenization/Book/Ch04/Theorems/Mu.lean(the a.e. endpoint and the statement-check note explaining why it is a.e.).
A genuinely LocalSigmaR (cubeSet Q)-measurable function on the honest carrier
agreeing with the coarse-grained energy Mu at every field lying in some
countable a.e.-elliptic quantitative slice of the cube. This is CoarseGraining's
exists_isLocalRandomVariable_ae_eq_Mu_cubeSet assembly with the
everywhere-on-the-covered-locus equality retained instead of discarded.
The coarse-grained energy of a measurable, everywhere locally a.e.-uniformly elliptic carrier source is genuinely measurable.
The upper-left coarse block b(Q; a) of a measurable, everywhere locally
a.e.-uniformly elliptic carrier source is genuinely measurable.
The lower-right coarse block σ_*⁻¹(Q; a) of a measurable, everywhere
locally a.e.-uniformly elliptic carrier source is genuinely measurable.
The operator norm of the upper-left coarse block is measurable.
The operator norm of the lower-right coarse block is measurable.
The descendant maximum of upper-left coarse block norms is measurable.
The descendant maximum of lower-right coarse block norms is measurable.
The weighted upper-block series is measurable.
The weighted lower-block series is measurable.
Finite-exponent upper multiscale ellipticity of a measurable, everywhere locally a.e.-uniformly elliptic carrier source is measurable.
Infinity-exponent upper multiscale ellipticity of a measurable, everywhere locally a.e.-uniformly elliptic carrier source is measurable.
Finite-exponent inverse lower multiscale ellipticity of a measurable, everywhere locally a.e.-uniformly elliptic carrier source is measurable.
Infinity-exponent inverse lower multiscale ellipticity of a measurable, everywhere locally a.e.-uniformly elliptic carrier source is measurable.
Full finite-or-infinite upper multiscale ellipticity measurability.
Full finite-or-infinite inverse lower multiscale ellipticity measurability.