High-contrast homogenization: Entry.Response.Kernel.SharpOrderEnergyMap #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The sharp-order layer of the coarse energy map #
Given the extra hypothesis ordering the primal and adjoint coarse blocks, this file sharpens the
coarse energy-map comparison of the diagonal weak-norm estimate: it bounds the Loewner order of the
recentred block by a scalar multiple of the sharp companion swapSharp, transports that bound
through the block congruence, and records the monotonicity, block-diagonal form and scalar action
of swapSharp these steps use. These are the sharp-order steps of the response-transfer
proposition p.response.transfer.
The sharp (primal-adjoint) order layer: the hypothesis hcmp supplied #
Nothing here restates or weakens any existing declaration, and the target
diagonalWeakNorm_primal_le in DiagonalWeakNormBound.lean is untouched.
Why this module exists #
The energy-map comparison energy_map_congr_le in
RecentScaleEnergyRoute.lean has a shared root for two consumers, and what both
consumers still share is exactly one hypothesis: its hcmp, the form used here of
diagonalMetric_le_scaled_coarseStarred_adaptedCellAtCenter. That hypothesis is supplied here,
and the comparison is discharged with it.
The design decision, and why no definition is introduced #
Two routes encode the same comparison. The first goes through
blockSharp, fullBlockSharp, relSize, blockSize, diagonalWeakMetricFactor,
metricBlockNormSq, adaptedResponse and adaptedDomainAt: eight new definitions, all
currently zero declarations in this development. The second expresses the comparison through
the carriers already present, and this module takes it.
This module introduces no definition at all. Every declaration below is a theorem, so no
satisfiability obligation arises from a definition. The two substantive hypotheses that do
carry content — positive definiteness and sharp self-duality of the reference block — are
hypotheses of theorems, and their satisfiability is nevertheless proved outright, in this module
and before the consumer statements that use them: the witness R = M_0(F)^{1/2} that the
consumers actually print is exhibited as an explicit ∃.
The three encodings needed and already available:
fullBlockSharp H = 𝐑 H⁻¹ 𝐑is written out as the literal producttoFullBlockMat (blockSwap d) * H⁻¹ * toFullBlockMat (blockSwap d);blockSwap(Setup/ProjectiveDistance.lean) isBook.Ch02.blockR, that isfullBlockRefl, on the nose;relSize P Q = ‖matSqrt Q⁻¹ * P * matSqrt Q⁻¹‖is definitionally‖toFullBlockMat (normalizedBlock P Q)‖(Setup/ProjectiveDistance.lean);blockSharp (coarseBlockMatrix U a) = coarseStarredBlockMatrix U a, which needs no positivity at all because𝐑is an involution.
Two simplifications of the route #
- The sharp comparison replaces the sizes
EagainstMandAagainstEby arbitrary positivekandecarrying only the two Loewner inequalities the proof uses. That is strictly more general, and it is the shape a consumer has: consumers own bounds on the two sizes, not their exact values. A separate size step recovers the exact-size instance when a consumer wants it. - The self-duality step goes through
blockMatInv_metric_eq_blockReflect; here it is done as the direct2 × 2block computation, so that lemma is not needed.
The route below is proved directly on the carriers of this development and of CoarseGraining;
nothing is imported from any other development and no file is copied.
The reflection and the sharp map on the flattened carrier #
The flattened reflection is its own transpose.
The flattened reflection is its own inverse.
The sharp map reverses the Loewner order.
The sharp map is homogeneous of degree minus one.
Dilation by a nonnegative scalar is monotone for the Loewner order.
The two-step sharp comparison #
The sharp comparison. If the reference block M is its own sharp, then two
Loewner comparisons E ≤ k M and A ≤ e E reverse under the sharp involution into a single
comparison of M against the sharp of A:
M ≤ (k e) · 𝐑 A⁻¹ 𝐑.
The sizes E against M and A against E are replaced by arbitrary positive k and e
carrying only the two inequalities the proof actually uses. That is strictly more general than
fixing those sizes, and it is the shape a consumer has: consumers carry bounds on the two sizes,
not their exact values.
The starred coarse block is the sharp of the coarse block #
The starred coarse block. On the flattened carrier the Chapter 2 starred coarse
response 𝐀_*(U;a) is the sharp of the ordinary coarse response, 𝐑 𝐀(U;a)⁻¹ 𝐑.
The route needs no positivity at all: 𝐑 is an involution, so (𝐑 X 𝐑)⁻¹ = 𝐑 X⁻¹ 𝐑
unconditionally.
The relative size, on the normalizedBlock carrier #
The size step. A block is dominated by its reference, dilated by the operator norm of
the Q-normalized block:
P ≤ |Q^{-1/2} P Q^{-1/2}| · Q.
No new definition is needed for the relative size: toFullBlockMat (normalizedBlock P Q)
unfolds to exactly matSqrt Q⁻¹ * P * matSqrt Q⁻¹, so
‖toFullBlockMat (normalizedBlock P Q)‖ is ‖matSqrt Q⁻¹ * P * matSqrt Q⁻¹‖ on the flattened
carrier. The proof is one observation: conjugation by Q^{-1/2} is a congruence sending Q
to 1, and the spectral norm reads a bound against 1 off directly.
The hypothesis hcmp, supplied #
hcmp, in general form. The reference block M, self-dual under the sharp
involution, is dominated by the starred coarse response of (U; a), dilated by the product of
the two size constants.
This is the hypothesis hcmp of the energy-map comparison, the form used here of
diagonalMetric_le_scaled_coarseStarred_adaptedCellAtCenter. Route: the sharp comparison on the
flattened carrier, then the identification of 𝐑 𝐀⁻¹ 𝐑 with 𝐀_*, then
blockMatLoewnerLE_of_le back into the block dialect. No new definition is introduced, and
no sharp involution is named in the statement.
hcmp in the form consumed. The general form with the reference block taken to be the
congruence R^T I R.
The self-duality hypothesis is satisfiable, with an explicit witness #
The self-dual diagonal metric. The diagonal metric diag(m, m⁻¹) is its own sharp.
The proof is the direct 2 × 2 block computation.
Congruence by the block square root. Congruence of the identity by the block square
root returns the block: (A^{1/2})^T I A^{1/2} = A. This is what makes the congruence shape
and the diagonal-metric shape the same statement.
The comparison discharged #
The comparison with its hcmp discharged. The shared root of the two consumers, with
no Loewner hypothesis left: the R-metric size of the doubled cell average is controlled by
the cell energy, as soon as the reference E sits between the metric root and the coarse
response with the two size constants k and e.
This is energy_map_congr_le in RecentScaleEnergyRoute.lean composed with the
preceding form of hcmp.
The comparison discharged on the metric root, the shape both consumers print.
The preceding theorem with R := M_0(F)^{1/2}, whose two hypotheses are discharged outright by
the explicit witness. What remains are exactly the two size inputs each consumer already owns:
a reference E squeezed between the metric M_0(F) and the cell's coarse response.
blockVecDot (M_0^{1/2} (Y)_U) (M_0^{1/2} (Y)_U) ≤ (k e) ⨍_U Y·𝐀Y.