LocalizationFluctuationMuMeasCore #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The field-slope doubled minimum as a countable infimum #
Internal Provider infrastructure for the Step-2 endpoint of
l.approximate.recurrence.formula.
The problem #
LocalizationFluctuationSelectValue.doubledMuField U a F is an sInf over the
uncountable affine class F + (L^2_{pot,0} x Lsolo)(U). The Step-2 endpoint
integrates it in the sample, so it has to be measurable in the sample; but the
sample enters through both the coefficient a and the slope field F, and
an sInf over an uncountable family carries no measurability by itself.
What this module does #
It replaces the uncountable infimum by a countable one, at a family of competitors that depends on the domain only:
exists_countable_doubledMuFieldCompetitors produces one sequence
D : ℕ → DoubledField d of test fields on U such that for every
Chapter-2 coefficient a : CoeffOn U and every vector-L^2 slope field F,
doubledMuField U a F = ⨅ n, doubledMuValue U a (F + D n) .
The sequence is produced once and for all from the second countability of
L^2(U; R^{2d}); the identity then holds pointwise in (a, F), so composing
with a sample gives an iInf of countably many sample functions. Measurability
of the field-slope minimum therefore reduces to measurability of the
fixed-competitor energies, which is the shape of upstream's own
FixedCompetitorEnergyMeasurability layer.
No measurable selection of a minimizer occurs, and nothing below asserts that a
minimizer exists: the statement is an identity between an sInf and a countable
sInf, valid whether or not the infimum is attained. The choice used to name
the sequence is choice on a countable dense subset of an L^2 ball of test
fields --- an internal object that occurs in no source-facing statement.
Method #
For a fixed U the affine class is F + T(U) with T(U) the (sample- and
coefficient-independent) set IsDoubledTestField U. Upstream's Hilbert layer
identifies the doubled energy of a field with the quadratic energy of its L^2
class under a coercive symmetric bilinear form
(MuOperatorRealization.quadraticEnergy_eq_blockEnergyAverage_of_blockState),
which is continuous on L^2 and nonnegative. L^2(U; R^{2d}) is
second countable (MeasureTheory.Lp.SecondCountableTopology), hence so is the
set of L^2 classes of test fields, which therefore has a countable dense
subset; pulling representatives back gives D. Continuity of the energy along
the L^2 class transfers the infimum.
References #
- ABK26,
l.approximate.recurrence.formula, the twoargmindisplays, Step 2,e.variational.mu.U.P.
L² bookkeeping #
The zero doubled field is a test field.
The L² class of a pointwise sum of block fields is the sum of the classes.
Adding a test field to the slope field returns to the affine class.
Nonnegativity and the two elementary bounds on the field-slope minimum #
Reproved here from the a.e. ellipticity of the Chapter-2 coefficient; the same
two steps occur in the proved local provider
Provider.Whitney.SubadditivityCountable.{blockEnergyDensityAt_nonneg_ae, doubledMuValue_nonneg}, which is a different cone and is deliberately not
imported.
The doubled energy density is a.e. nonnegative on the domain, because the coefficient is a.e. elliptic there.
Every doubled energy value is nonnegative.
The field-slope value set is bounded below by 0 and nonempty.
The field-slope value set is nonempty: the slope field is its own competitor.
The lower bound on the field-slope minimum. Unconditional.
The upper bound on the field-slope minimum by any competitor's energy. Unconditional; the competitor is supplied by the caller as a member of the affine class.
The upper bound at the slope field itself. Unconditional.
The countable competitor family #
The field-slope doubled minimum is a countable infimum.
For every Chapter-2 domain U there is one sequence D of test fields on U,
depending on U alone, such that for every coefficient a : CoeffOn U and
every vector-L^2 slope field F the canonical number
doubledMuField U a F is the greatest lower bound of the countable set of
energies doubledMuValue U a (F + D n).
No minimizer is selected and none is assumed to exist: this is an identity
between the sInf of an uncountable value set and the sInf of a countable
subset of it.
The named competitor family and the measurability reduction #
The canonical countable competitor family of the field-slope problem on
U. A sequence of test fields depending on the domain only; it names the
sequence produced by exists_countable_doubledMuFieldCompetitors. It occurs in
no source-facing statement: it is an internal index for the countable infimum
below.
Equations
Instances For
Each canonical competitor is a test field on U.
The field-slope minimum is the greatest lower bound of the canonical countable family of competitor energies.
The field-slope minimum as a countable infimum. This is the identity that makes the Step-2 endpoint integrand measurable in the sample.
The measurability reduction. If the sample-dependent coefficient and slope field make every fixed-competitor energy measurable, then the field-slope minimum is measurable. No minimizer is selected anywhere: the conclusion is obtained from the countable-infimum identity.
The integrability reduction. The field-slope minimum is squeezed
between 0 and the energy of the slope field itself, so it is sample-integrable
as soon as it is measurable and that one fixed competitor's energy is
integrable. No estimate on the minimum is used.