LocalizationFluctuationJointField #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The sample-dependent competitor: from a fixed field to a measurable L^2 class #
ABK26, l.approximate.recurrence.formula, Step 2.
The obligation this module discharges #
LocalizationFluctuationJointCoeff.measurable_doubledMuValue_meshCellCoeff
makes the doubled energy value measurable in the sample when the competitor
field is fixed. The Step-2 integrand needs it when the competitor moves
with the sample as well: the background of the field-slope problem is
P_z(omega) + bfF_z(omega), whose two legs are read along the corrector
family. This module removes the fixed-field restriction, at the only cost that
is unavoidable: the competitor must be presented through a measurable L^2
class, not through a pointwise family.
Method #
For a fixed coefficient a the doubled energy value is a continuous function
of the L^2 class of the competitor: this is CoarseGraining's own Hilbert
realization of the doubled problem
(MuOperatorRealization.quadraticEnergy_eq_blockEnergyAverage_ of_blockState
together with quadraticEnergy_continuous), packaged here as
exists_continuous_doubledMuValue_of_class. Composing:
- in the class variable the energy is continuous, for every sample;
- in the sample variable it is measurable, for every fixed class --- because
every class is the class of some honest block field
(
exists_memBlockL2_toHilbertBlockL2OfBlockField_eq, from the canonical strongly measurableLprepresentative), and at a fixed field the measurability is the previous module's.
MeasureTheory.measurable_uncurry_of_continuous_of_measurable (Caratheodory)
then makes the two-variable energy jointly measurable, and composing with the
measurable class of the competitor finishes. HilbertBlockL2 is a separable
metrizable space, which is what the Caratheodory lemma asks of the index.
No measurable selection occurs. The competitor is not chosen: it is given,
and only its L^2 class is used. The block-field representative extracted from
a class is used solely as a witness inside a measurability proof; no statement
below mentions it.
Main results #
exists_memBlockL2_toHilbertBlockL2OfBlockField_eq--- surjectivity of the class map onto the doubledL^2carrier.exists_continuous_doubledMuValue_of_class--- the doubled energy value is a continuous function of the competitor'sL^2class.measurable_doubledMuValue_of_measurable_class--- the generic transfer.measurable_doubledMuValue_meshCellCoeff_of_measurable_class--- its instantiation at the Step-2 cell coefficient, which is the statement thehcompbinder ofLocalizationFluctuationMuMeasCell.integrable_meshFluctuationCellIntegrand'and the measurability half of itshbgbinder both reduce to.
Binders #
Beyond the typing binders: [NeZero d]; the L^2 membership of the competitor
at every sample (a typing property of the corrector data, not an estimate); and
measurability of its class. No integrability, no ellipticity constant, no
smallness and no estimate occurs.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formula, Step 2, the twoargmindisplays,e.variational.mu.U.P.
Every doubled L^2 class is the class of an honest block field #
Surjectivity of the class map. The canonical Lp representative of a
doubled L^2 class is a strongly measurable block field whose class is the
given one. No choice beyond Lp's own representative occurs.
The energy as a continuous function of the competitor's class #
The doubled energy value is a continuous function of the competitor's
L^2 class.
For every Chapter 2 domain and every coefficient there is a continuous real
function on the doubled L^2 carrier which returns doubledMuValue at the
class of any block-L^2 doubled field. This is CoarseGraining's Hilbert
realization of the doubled problem, read at a fixed coefficient; it is the
exact ingredient LocalizationFluctuationMuMeasCore already uses to transfer
an infimum, exported here on its own.
The transfer #
The doubled energy value at a sample-dependent coefficient and a
sample-dependent competitor is measurable, as soon as the competitor's L^2
class is.
The competitor family X is arbitrary: no measurability of omega |-> X omega
as a family of functions is assumed, and no minimizer or representative is
selected. Only the class map omega |-> [X omega] is asked to be measurable,
which is the shape the proved corrector-gradient measurability delivers.
on hX (block-L^2 membership at every sample, a typing property), hclass,
and hfixed --- measurability in the sample at every fixed competitor with
measurable components, which
LocalizationFluctuationJointCoeff.measurable_doubledMuValue_meshCellCoeff
supplies at the Step-2 carriers.
The Step-2 instantiation. At the cell coefficient meshCellCoeff M m R
the fixed-competitor measurability is proved
(LocalizationFluctuationJointCoeff.measurable_doubledMuValue_meshCellCoeff),
so a measurable L^2 class of the competitor is all that is needed.
This is the joint-measurability layer's payoff: it turns the hcomp binder of
LocalizationFluctuationMuMeasCell.integrable_meshFluctuationCellIntegrand', and
the measurability half of that lemma's hbg binder, into the single statement
"the background field's L^2 class is a measurable function of the sample".