Stability #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
Per-phase stability of the corridor observable #
Statement of p.phase.comparison's stability estimate e.phase.comparison.stability
in the discrete-grid setting. With U := cubeSet (originCube d m),
S := corridorSet ℓ σ, and Z the minimizer for (a, P)
(exists_cubeBlockMinimizer, which supplies Mu U P a = blockEnergyAverage U a Z):
F := P·𝐀(U; a)P = 2·Mu U P a, and2·Mu U P a = (vol U)⁻¹ ∫_U Z·(blockCoeffField a)Z(coarseBlockMatrix_quadratic_eq_energyIntegral); the sharp constant is24Θ = (vol U)⁻¹·6·(4Θ). We state the (weaker, still true)48Θ, valid because the corridor energy integrand is≥ 0(blockMatrixOfCoeff_quadratic_nonneg).- B′3
abs_setIntegral_energy_sub_lewithB := blockCoeffField a,Bt := blockCoeffField (corridorField ℓ σ a),S := corridorSet ℓ σ ∩ U, minimizersZ(fora),Zσ(forcorridorField ℓ σ a, elliptic viacorridorField_isEllipticMatrix).
The general B′3 assembly is abs_coarseObservable_sub_le_of_minimizer;
abs_phaseObservable_sub_le_of_minimizer specializes it to the corridor field.
abs_phaseObservable_sub_le (M2) is the existential wrapper. The Z-as-input
form is what grid averaging needs, since one minimizer serves every phase σ.
Field-level ellipticity transport through the corridor #
The corridor self-map preserves everywhere-(1, Θ)-ellipticity on U: the
pointwise ellipticity is corridorField_isEllipticMatrix, and the entrywise
measurability of the U-truncated modified field is the corridor-gated
piecewise of the constant (1 : Mat d) and the original truncated field.
The Mu-quadratic as a normalized energy integral #
P·𝐀(U; a)P = (vol U)⁻¹ ∫_U Z·(blockCoeffField a)Z for any minimizer Z
of (a, P) on the half-open triadic cube. This is Mu = ½ P·𝐀 P combined with
Mu = blockEnergyAverage, the ½ cancelling the density's ½.
The general two-field coarse-stability lemma (B′3 core) #
General coarse stability. For two fields c, c' that are (1, Θ)-elliptic
on U := cubeSet (originCube d m) and agree on U ∖ S, the coarse observable
moves by at most 48 Θ (vol U)⁻¹ times the S-energy of any minimizer Z
for c. This is the corridor-independent heart of
abs_phaseObservable_sub_le_of_minimizer.
M2: corridor specialization #
M2 core. Given the minimizer Z for (a, P) (its admissibility,
response-space membership and energy-realizing identity), the corridor-phase
comparison bound holds with the corridor energy of that specific Z. This is
a specialization of the general two-field bound; abs_phaseObservable_sub_le
obtains Z and calls this.
M2 (per-phase stability). For a fixed grid phase σ and a coefficient
a that is (1, Θ)-elliptic on U := cubeSet (originCube d m), the coarse
observable moves by at most a normalized corridor energy of the minimizer
Z for (a, P).