High-contrast homogenization: Entry.Response.Kernel.CoarseBlockPerCellInput #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The coarse-block identification and the per-cell energy-map input #
This file identifies the Chapter-2 coarse-block matrix of a recentred coefficient on an aligned
adapted cell with the shear congruence of the cell's set-level coarse block, for both signs. It
reduces the diagonal weak-norm estimate's remaining analytic hypothesis to two real-arithmetic
facts, and packages its per-cell hypothesis from either a bound by fixed constants or a bound by
the metric and the cell size. It then composes the recent-difference energy map with this
bookkeeping on an aligned cell, for the recentred sample and, tracking the extra congruence the
flux flip introduces, for its adjoint twin. It serves the weak-norm estimate
e.response.weak.estimate.
The Chapter-2 coarse block of an adapted cell is the shear congruence #
This module discharges the identification that the recent-difference and parent energy maps carry as an explicit hypothesis: the Chapter-2 coarse block matrix of the recentred coefficient on an aligned adapted cell is the shear congruence of the cell's set-level coarse block.
The two coarse-block carriers are not syntactically the same object. Chapter 2 builds the block
from the doubled variational quantity π(U; a) through the sigma/kappa recovery package,
while the set-level block is assembled directly from Mu by polarization. The two constructions
agree on every Chapter-2 domain: Chapter-2's doubledMu is the set-level Mu of the coefficient
field (book_doubledMu_eq_Mu), and a block is determined by its Mu quadratic form
(IsCoarseBlockMatrix and eq_coarseBlockMatrix_of_isCoarseBlockMatrix). That is the content of
coarseBlockMatrix_domain_eq_set.
The shear congruence itself is the set-level identity for a field recentred by a skew matrix: the
quadratic form of a x - g is the quadratic form of a at the sheared state
(p, g p + q), so the recentred block is Gα΅ π G. This is isCoarseBlockMatrix_respCoeffMinus;
the adjoint twin
isCoarseBlockMatrix_respCoeffPlus composes it with the flux sign flip D = diag(Id, -Id).
The Chapter-2 coarse block of a Domain is the set-level coarse block of its
representative. Chapter-2's doubledMu is the set-level Mu of the coefficient field, and a
symmetric block is determined by its Mu quadratic form, so the two constructions coincide.
The coarse block of a field on an aligned adapted cell satisfies the variational
characterization. A pointwise elliptic representative exists on the cell; CG's convex-domain
recovery supplies the Mu quadratic form for that representative, and Mu is insensitive to
changing the field on a null set.
The set-level shear identity from the variational characterization. If the set-level
coarse block of a is characterized by Mu, then recentring by a skew matrix g turns the
recentred block into the congruence of the block by G = ((1, 0), (g, 1)). This is the
IsCoarseBlockMatrix form of the shear step, which avoids a separate quadraticity hypothesis.
The recentred coarse block of an aligned cell is the shear congruence of the cell's coarse
block, minus sign. This is the identity the recent-difference energy map consumes: the
Chapter-2 block of the recentred coefficient equals Gα΅ π G for the cell's set-level coarse
block.
The recentred coarse block of an aligned cell is the composed congruence of the cell's
coarse block, plus sign. The recentred adjoint field is respCoeffPlus F a = aα΅ + g, so the
shear identity applies at the adjoint field with skew -g, and the adjoint block is the flux
sign flip D of the primal block. This matches the hcoarse shape of the adjoint energy map.
The analytic per-scale input, reduced to its two analytic facts #
What this file does and does not do #
recentHead_actual_le (DiagonalWeakNormAssembly.lean) has exactly ONE
remaining hypothesis, its hscale: the analytic per-scale bound on the average-defect family.
That bound is diagonalWeak_recent_average_bound.
Reading the proof of that theorem, its content splits cleanly in two:
- an algebraic spine β per-cell bound, average, CauchyβSchwarz-free
βalgebra β which is pure real arithmetic over aFinset; and - two analytic inputs,
metricBlockNormSq_recent_difference_leanddiagonalWeak_recent_difference_energy_le, which are PDE facts about the doubled response space.
This file proves the spine and states the two analytic inputs as explicit hypotheses in
this tree's own language. It does NOT prove those two inputs; their root
energy_map_metric_le rests on
doubledResponseValue_le / doubledResponseValue_zero_left_eq and
on the reflection-order layer (blockSharp, 444 lines plus its
VariationalIdentities.lean base of 323), none of which exists in this tree OR in the
CoarseGraining dependency.
What is gained is nonetheless the substance of the bound: after this file, the per-scale bound
is reduced to TWO named inequalities, stated on this tree's carriers, whose
conjunction discharges hscale mechanically.
Nothing is imported from an external development and no file is copied; the spine is stated on
this tree's inline β(|Z|β»ΒΉ β βͺΒ·,Β·β«) carrier, which is
what weakCellSum, h6a_besovSeminorm_head_tail_le and hscale all spell.
The algebraic spine of the per-scale input, on an arbitrary index Finset.
This is diagonalWeak_recent_average_bound
with its two analytic inputs abstracted into the hypotheses hcell and henergy, and with
blockAvsumL2 unfolded to this tree's inline β(|Z|β»ΒΉ β βͺΒ·,Β·β«).
hcell is the per-cell bound assembled from metricBlockNormSq_recent_difference_le
together with the all-scale-maximum bound on the response size; henergy is
diagonalWeak_recent_difference_energy_le. Everything after them is real arithmetic β
Finset.sum_le_sum, a nonnegative rescaling, and β(cΒ²x) = cβx.
The spine at the exact shape of hscale. #
The per-scale input, reduced to its two analytic inputs. This is scaleInput_spine_le
instantiated at exactly the shape of the remaining hypothesis hscale
(recentHead_actual_le, DiagonalWeakNormAssembly.lean): the index set is
triadicIndexBox d n, the root is blockSqrt (respM0 F), and the four scalars are the printed
ones β
K = β(blockSpecBound (normalizedBlock Γβ» Mβ)), thediagonalWeakMetricFactor m E;B = 1 + β(respAllScaleMax) Β· 3^{Οn/2}, the all-scale-maximum factor;L = β(respLsqMinus), thediagonalWeakLoadMinus E p r;D = βweakAverageDefect β¦β, theblockSize (diagonalWeakAverageDefect β¦) (blockIdentity d).
The field family Y is left abstract: recentHead_actual_le instantiates it at
Y w = fun x => optimizerField b u x - optimizerField b (V n w) x, which matches definitionally.
The two hypotheses are precisely the two analytic inputs, in this tree's language:
hcellismetricBlockNormSq_recent_difference_lecomposed with the response-size boundblockSize (adaptedResponse β¦) E β€ BΒ², which is derived fromsqrt_blockSize_adaptedResponse_le_of_maximum_finite;henergyisdiagonalWeak_recent_difference_energy_le.
Neither is proved in this tree. What this theorem establishes is that NOTHING ELSE is needed:
given those two, hscale follows mechanically, and with it the entire first printed
summand of diagonalWeakNorm_primal_le.
The per-cell hypothesis of the per-scale input, from its two inputs #
The per-scale input scaleInput_of_analytic consumes a per-cell hypothesis bounding the
metric square of a cell average by a fixed printed constant times a weight G. The energy-map
layer delivers that bound with a different constant: a product k * e of two Loewner sizes.
This file is the bookkeeping that turns the second shape into the first, given the numerical
comparison between the two constants.
Both statements are monotonicity of multiplication by a nonnegative weight. No matrix identity is used beyond the nonnegativity of the quantities involved, and the first statement is the generic core of the second.
Monotonicity of a per-cell bound in its constant. If V w β€ cβ * G w for every w in a
finite index set and the weight G is nonnegative there, then the same bound holds with any
larger constant cβ. The nonnegativity of cβ is carried because the constant in the analytic
per-scale input is a product of Loewner sizes, but the monotonicity step itself needs only
cβ β€ cβ and 0 β€ G w.
The per-cell hypothesis of the per-scale input, obtained from the energy-map bound. The
cell-average metric square is bounded by (k * e) * G w for the two Loewner sizes k and e;
the comparison hsize turns the product into the printed square
(βKβ Β· (1 + βM Β· 3^{Οn/2}))Β², and the nonnegative weight yields the conclusion. The index set
is triadicIndexBox d n, the root is blockSqrt (respM0 F), and the two constants and the
response sample are those of the weak-norm estimate (e.response.weak.estimate).
The recent-difference energy map on an aligned cell #
This composes the recent-difference energy map on the doubled response space with the per-cell bookkeeping of the weak-norm estimate. The response-size input is taken at the square of the printed geometric factor, and the metric factor is the operator norm of the normalized reference block, which on positive definite carriers is the printed spectral bound.
The remaining input is the identification of the Chapter-2 coarse block with the shear
congruence of the cell's coarse block. The two coarse-block carriers used here β the Chapter-2
coarseBlockMatrix on a Domain and the set-level coarseBlockMatrix on the cell β are not
identified by any declaration in this module's import closure, so that identification is carried
as an explicit hypothesis.
The recent-difference energy map on an aligned cell, with the response-size factor supplied
through the shear congruence. For every index w in the triadic box, the metric square of the
cell average of the doubled difference of two optimizers is bounded by the printed geometric
square times the actual difference energy on that cell.
The hypothesis hcoarse identifies the Chapter-2 coarse block of the recentred coefficient with
the shear congruence of the cell's coarse block; it is the shape the shear identity produces and
the one input this module cannot discharge from its own imports.
The recent-difference energy map, adjoint sign, as a split proof #
The energy map of CoarseBlockPerCellInput is stated for the recentred sample
respEhatMinus. The + copy of the cell-average estimate needs the adjoint twin, whose sample
is respEhatPlus = blockAdjoint (respEhatMinus β¦). Because the adjoint adds one congruence by
the flux flip D, the response-size input is no longer a bound for the shear factor respG F
alone: it is the composed factor D β respG F. This file splits the port in two so that the
large block terms are elaborated once each: the per-cell step carries the two Loewner constants
abstract, and the second theorem feeds it the adjoint size inputs.
The remaining input of the second theorem is the identification of the Chapter-2 coarse block of
the recentred adjoint field with the composed congruence of the cell's coarse block; the two
coarse-block carriers used here β the Chapter-2 coarseBlockMatrix on a Domain and the set-level
coarseBlock on the cell β are not identified by any declaration in this module's import closure,
so that identification is carried as an explicit hypothesis, exactly as for the minus sign.
The per-cell step of the recent-difference energy map for the adjoint sample, with the two
Loewner constants abstract. This is recent_difference_metric_le
(ResponseFieldSize.lean) instantiated at an aligned child cell and the doubled
optimizer difference: the reference sample is respEhatPlus, the root is blockSqrt (respM0 F),
and arbitrary positive k, e are supplied through the two Loewner hypotheses hEM, hAE.
The recent-difference energy map on an aligned cell for the adjoint sample. This is the
adjoint twin of recentEnergyMap_port (CoarseBlockPerCellInput.lean): the
sample is respEhatPlus, and the response-size input hcoarse identifies the Chapter-2 coarse
block of the recentred field with the composed congruence D β respG F, the factor the adjoint
carries. The per-cell step is recentEnergyMap_cell_plus above.