High-contrast homogenization: Entry.Response.Kernel.OptimizerEnergyIdentity #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The optimizer-energy identity and the energy split on {M > 1} #
For a response maximizer of a load (p, q), the squared pathwise optimizer energy equals twice
the response value, ℰ² = x · A(U) x - 2(p · q) = 2J, and this file proves that identity - via
a first-variation (Euler-Lagrange) argument for IsResponseMaximizer, since no available
identity reaches the Dirichlet energy directly - together with its instances at the recentred
and adjoint coefficients. It also proves the resulting energy-split bound on the event {M > 1}
of the all-scale maximum, p.response.transfer.
The energy split on {M > 1} (p.response.transfer) #
The energy identity, the depth-0 extraction, congruence and un-normalization #
The statement is dealt with in four steps.
(i) ENERGY IDENTITY. By definition
ℰ_t(a)² = volumeAverage U_t (x ↦ ∇v_a(x) ⬝ b_a(x) ∇v_a(x)).
For a response maximizer u of the load (p, q) for b on U the identity needed is
volumeAverage U (∇v ⬝ b ∇v) = x ⬝ (coarseBlockMatrix U b) x - 2 (p ⬝ q), x = (-p, q),
i.e. ℰ² = 2 J = x ⬝ A(U;b) x - 2 (p ⬝ q) with J = ResponseJ U p q b. What is available
is
* the MEAN identity cellAverage_optimizerField_eq_blockResponseMean
: the cell average of (∇v, b∇v) is x + 𝐑 A(U) x; and
* the RESPONSE-VALUE identity ResponseJ U p q b = ½ x ⬝ A(U) x - p⬝q, used inside that
proof and exported as
Annealed.responseJ_eq_coarseBlock_adapted.
Neither says anything about the maximizer's Dirichlet ENERGY. CoarseGraining's
ResponseIdentities/AverageFormulas/CoarseFormulas.lean is the only candidate and it is
(a) only the p = 0 case, (b) only under IsSigmaStarCoarse, and (c) only an inequality.
The identity is therefore supplied below by a first-variation lemma (the Euler-Lagrange
identity for IsResponseMaximizer), not by reassembling the identities above.
(ii) DEPTH-0 EXTRACTION. The bound
A_t(a) ≤ (1 + M(a)) E_t comes from M(a) ≥ 3^{-ρ·0}·blockSpecBound(normalizedBlock (A_t(a)) E_t - I), i.e. from le_csSup applied to the n = 0, z = 0 member of the defining set of
respAllScaleMax (ResponseBlockObjects.lean; triadicIndexBox d 0 = {0} and
adaptedCellAtCenter q (t-0) 0 = adaptedCell q t are routine). le_csSup needs BddAbove
of that
set. Without it the sSup is the junk value 0 and the inequality is FALSE (take any a
whose coarse blocks blow up along n: M(a) = 0 while A_t(a) is not ≤ E_t). This is why
the statement carries the qualification ∀ᵐ a ∂P. That BddAbove is derivable pathwise from
RawOutput alone and with no new binder; it is proved below as pathwise_envelope and
consumed by coarseBlock_le_one_add_respAllScaleMax. The bound comes from
Source.bounded_source_envelope (HCPoly/Entry/Source/BoundedWindowFiniteness.lean,
sorry-free),
whose only hypotheses are IsStationaryLaw P and CoarseEllipticityDagger P γ E Ψ K Src --
raw.stat and raw.ell. See the block below for the full argument.
(iii) CONGRUENCE. coarseBlockMatrix U_t (respCoeffMinus F a) = blockCongr (respG F) (coarseBlock U_t a)
is coarseBlockMatrix_sub_skew_eq_blockCongr. It consumes
HasQuadraticMu U_t (a.1 : CoeffField d), which RawOutput does not state: the congruence
lemmas take it
as the explicit hypothesis hquad. That datum is a theorem on
every adapted cell, hasQuadraticMu_adaptedCell below, whose only hypothesis
IsUnit (respGrid jStar F) is itself discharged from RawOutput by
isUnit_respGrid_of_rawOutput below, so no binder is added to the statement.
(iv) UN-NORMALIZATION. A_t(a) ≤ (1+M) E_t gives, by congruence with respG F,
x ⬝ A^{b^-}_t(a) x ≤ (1+M) · x ⬝ Ehat_t^- x = (1+M) (L^-)²
(le_smul_of_normalizedBlock_le_of_posDef,
HCPoly/Entry/Response/Core/AnnealedMeanDrift.lean, and Analysis.matrix_congr_le).
The first-variation lemma and the sign of the p·q term #
Step (i) is proved below and step (iii) is not a missing premise.
The identity is supplied by the first-variation lemma responseJ_energy_of_isResponseMaximizer
(CoarseGraining/ResponseIdentities/Foundations/Ellipticity.lean), proved there from
basic_cg_identities_first_variation_of_isResponseMaximizer (the Euler-Lagrange identity,
same file) and volumeAverage_scalarResponseIntegrand_eq_firstVariation_self_add_half_energy.
Its integrability premises are discharged by
ResponseLinearIntegrabilityData.of_isEllipticFieldOn
(ResponseIdentities/Foundations/Maximizer.lean). This tree's weakOptimizerEnergy
is already the scalar energy ⨍ ∇v·b∇v, and
vecDot_matVecMul_symmPart (Ambient/CoefficientField.lean) identifies it with
scalarVariationEnergyIntegrand. The block form below is the identity
responseJ_eq_block_quadratic_of_isOpenBoundedConvexDomain.
SIGN RESOLUTION (the −2p·q vs +2p·q discrepancy in the block above). Writing both sides with
this tree's actual definitions:
ResponseJ U p q b = ½ (−p,q)·A(U;b)(−p,q) − vecDot p q(Annealed.responseJ_eq_coarseBlock_adapted,HCPoly/Entry/Annealed/AdaptedDomainLocality.lean);weakOptimizerEnergy U b u ^ 2 = 2 · ResponseJ U p q b(step (i), below). EliminatingResponseJgivesℰ² = x·A(U;b)x − 2 (p·q),x = (−p,q): exactly the identity displayed in the block above. The block's own gloss "ℰ² = 2 J + 2 p⬝qwithJ = ResponseJ U p q b" is internally inconsistent with its own display two lines earlier (it would forceℰ² = x·A x); so is the docstring's "ℰ_t^2 = 2J_t = x^-·A^b_t(a)x^-". No sign was adjusted to make a proof close: the four theorems below are proved from the identities as stated, and the−2 (p·q)is what comes out. The residual−2 (p·q)is harmless for the statement, whose conclusion is an upper bound: on the selected loadsvecDot p q^∓ = 1(vecDot_respP_respqMinus_eq_oneandvecDot_respP_respqPlus_eq_one,HCPoly/Entry/Response/Core/ResponseCalibrationBundles.lean, fromp·q = e·e = 1and the skewness ofg − h_t), so the term is−2 ≤ 0.
STEP (iii) IS NOT A MISSING PREMISE. The statement is not "under-hypothesised" by
HasQuadraticMu U_t (a.1 : CoeffField d): that datum is a THEOREM on every adapted
cell, hasQuadraticMu_adaptedCell below (re-proved from the sorry-free
hasQuadraticMu_adaptedCellTranslate, HCPoly/Entry/Response/Core/SourceLoadBound.lean), and its
only hypothesis
IsUnit (respGrid jStar F) is itself discharged from RawOutput by
isUnit_respGrid_of_rawOutput below (raw.hj, raw.symm, raw.pos). So no binder is added to
the statement.
STEP (ii). le_csSup on the defining set of
respAllScaleMax (ResponseBlockObjects.lean) needs a.e. BddAbove of
{3^{−ρn} · blockSpecBound (normalizedBlock (coarseBlock (adaptedCellAtCenter q (t−n) z) a) E_t − I)}
over all n : ℕ and z ∈ triadicIndexBox d n. This is proved below.
The pathwise envelope behind the a.e. BddAbove #
Step (ii) is derivable with no new hypothesis.
WHERE THE BOUNDEDNESS COMES FROM. Every cited declaration is sorry-free.
(1) HCPoly/Entry/Source/BoundedWindowFiniteness.lean Source.bounded_source_envelope. For any
BOUNDED region W it produces an auxiliary scale J and a measurable envelope X ≥ 0 with
∀ᵐ a ∂P, ∀ q, InverseNormLE q 2 → ∀ j y, adaptedCellTranslate q j y ⊆ W →
coarseBlock (adaptedCellTranslate q j y) a ≤ (Cd · X a · 3^{γ·max(J−j,0)}) E.
Its ONLY hypotheses are IsStationaryLaw P and CoarseEllipticityDagger P γ E Ψ K Src,
which RawOutput carries verbatim as raw.stat and raw.ell (ResponseBlockObjects.lean).
It carries no source threshold, which is why this estimate is available here
while the threshold estimate described below is not.
(2) The bounded region is U_t itself: adaptedCell_isOpenBoundedConvexDomain
, and every cell of the family lies in it --
adaptedCellAtCenter_subset_adaptedCell
(HCPoly/Entry/Response/Core/ScalarMaximizerExistence.lean). So the ellipticity constants are
fixed BEFORE the
scale index n is quantified. InverseNormLE (respGrid jStar F) 2 is
Geometry.inverseNormLE_roundedGrid (RoundedGridBasic.lean) from raw.hj and
raw.symm/raw.pos.
(3) The normalizer E_t is positive definite -- Annealed.adaptedMean_posDef
(HCPoly/Entry/Annealed/AdaptedCellFoundations.lean) -- so E ≤ κ E_t for SOME κ ≥ 0 by pure
linear algebra (exists_scale_le below, κ = ‖E_t^{-1/2} E E_t^{-1/2}‖). Only the
EXISTENCE of κ is needed, never its size; that is what lets this argument avoid
Annealed.adaptedMean_refBlock_normalization, whose source threshold the statement cannot
discharge.
(4) The decay 3^{-ρn} IS used: the envelope's own factor 3^{γ·max(J−j,0)} GROWS in
the depth n = t − j, and it is ρ = (1+γ)/2 ≥ γ (for γ < 1) that makes the weighted
family bounded -- in fact bounded by its n = 0 value. See pathwise_envelope.
THE THRESHOLD ESTIMATE IS NOT USED.
pathwise_bound_max (HCPoly/Entry/Response/Core/PathwiseFluctuationBound.lean) feeds
respAllScaleMax_le_of_forall a hypothesis that IS a
BddAbove witness, and it is already elaborated. But it consumes hpath from
Source.source_multiplier_and_adapted_bound and hnormt from
Annealed.adaptedMean_refBlock_normalization, BOTH of which require the source threshold
⌈Csrc_i · logb 3 (2K)⌉ ≤ j_* for constants Csrc_i they themselves produce. The all-scale
maximum bound can supply it because it produces Csrc
The statement quantifies Csrc
universally, so raw.hsrc cannot be specialised and that estimate is unavailable here WITHOUT a
statement change. The envelope estimate needs no threshold at all.
The helpers below are private in
HCPoly/Entry/Response/Core/AnnealedMeanDrift.lean and
HCPoly/Entry/Response/Core/PathwiseFluctuationBound.lean, and are re-proved here on
this tree's carriers. Those modules are already in this
file's import closure (via LoadMeanIdentity), but their helpers are private, so importing would
not have helped; no import was added.
step (i): the maximizer energy identity. #
ℰ² = 2 J = x·A(U;b)x − 2 (p·q), x = (−p, q). This is the first-variation lemma; the sign
of the p·q term is that of the block above.
Step (i), the maximizer energy identity in the form ℰ² = 2 J, for a pointwise elliptic
coefficient field. The Euler-Lagrange identity is
responseJ_energy_of_isResponseMaximizer (ResponseIdentities/Foundations/Ellipticity.lean)
on this tree's set-level carriers; the passage from
weakOptimizerEnergy's integrand ∇v·b∇v to scalarVariationEnergyIntegrand's ∇v·symm(b)∇v
is vecDot_matVecMul_symmPart.
Step (i), transported to the qualitative coefficient carrier: the identity holds for a
field b that is only a.e. equal to a pointwise elliptic representative, which is the only form
the carrier CoeffSpace d supports (same transport pattern as
bddAbove_respWeakEnergySet).
Step (i), in block form on an adapted cell: ℰ² = x·A(U;b)x − 2 (p·q), x = (−p, q).
This is the identity displayed above; note the sign of the p·q term.
Step (i) for the recentred sample a_- = a − g (p.response.transfer), on the carrier.
Step (i) for the adjoint sample a_+ = a^t + g (p.response.transfer), on the carrier.
step (iii): the congruence hypotheses #
Neither datum becomes a binder of the statement: both are theorems, provable from RawOutput
alone.
Step (iii.a). IsUnit (respGrid jStar F) is a consequence of RawOutput: raw.hj is
2d ≤ 3^jStar and raw.symm/raw.pos give (explicitCanonicalMetric F).PosDef.
Step (iii.b). HasQuadraticMu holds on every adapted cell for the qualitative
coefficient carrier, so it is not a missing premise of the statement. This specializes the
sorry-free
private hasQuadraticMu_adaptedCellTranslate
to y = 0.
Block A: the Loewner / blockSpecBound layer.
The quadratic form of blockIdentity.
The converse of specBound_sub_identity_le: from a spectral bound on A - I back to
A ≤ (1 + c) I, given any witness making the defining infimum attained.
Block B: un-normalization, the converse of normalizedBlock_le_scale
(HCPoly/Entry/Response/Core/PathwiseFluctuationBound.lean, public). The matrix algebra follows
the private
le_smul_of_normalizedBlock_le_of_posDef (HCPoly/Entry/Response/Core/AnnealedMeanDrift.lean),
rewritten in the
BlockMatLoewnerLE language so that no Matrix-order bridge is needed.
Undoing the normalization in block language: R^{-1/2} A R^{-1/2} ≤ c I gives
A ≤ c R.
Block C: the soft comparison of two fixed blocks. This is what replaces the
quantitative Annealed.adaptedMean_refBlock_normalization, whose threshold hypothesis the statement
cannot discharge. Only existence of a
constant is needed for BddAbove, and existence is pure linear algebra.
Block D: the envelope estimate -- the pathwise, a.e. bound on every weighted term of the
defining set of respAllScaleMax (ResponseBlockObjects.lean), hence its BddAbove.
The producer is Source.bounded_source_envelope
(HCPoly/Entry/Source/BoundedWindowFiniteness.lean, sorry-free), whose ONLY hypotheses are
IsStationaryLaw P and CoarseEllipticityDagger P γ E Ψ K Src -- both carried by RawOutput
as raw.stat and raw.ell. It carries no source threshold, which is what lets this estimate
avoid the threshold required by the estimate discussed above.
0 ∈ triadicIndexBox d n for every depth.
The pathwise all-scale envelope. For P-a.e. sample a there is
one constant C(a) that simultaneously (1) Loewner-dominates the depth-0 coarse block by
C · E_t and (2) bounds every weighted term of the defining set of respAllScaleMax.
The decay 3^{-ρ n} IS used: the window envelope's own factor 3^{γ·max(J-j,0)} grows in the
depth n = t - j, and it is ρ = (1+γ)/2 ≥ γ (for γ < 1) that makes the product summable --
in fact bounded by its n = 0 value.