High-contrast homogenization: Entry.Response.Kernel.DiagonalWeakNormBound #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The diagonal weak-norm primal bound (Lemma 2.16) #
This file proves the two tail branches of the cell-average estimate for the recentred coefficient
a_- = a - g: it bounds the normalized scale-average seminorm of the recentred,
metric-transported subcell averages of the doubled optimizer field, in two branches according to
the size of the all-scale maximum M. It then states and proves the diagonal weak-norm primal
bound itself, diagonalWeakNorm_primal_le - HC bridge II, paper p.response.transfer,
Lemma 2.16 - assembled from the recent head estimate and the older-scale tail bound.
The two tail branches of the cell-average estimate at the carriers #
The cell-average estimate e.response.weak.estimate bounds the normalized scale-average seminorm
of the recentred, metric-transported subcell averages of the doubled optimizer field of the parent
adapted cell, 3 ^ (-(t / 2)) * besovSeminorm t, in two branches according to the size of the
all-scale maximum M = respAllScaleMax P γ jStar F t a. Every input of the older-scale branch is
already proved at the estimate's own carriers: the per-cell bound tailCell_of_bridge, the
per-scale assembly scaleTail_carrier, the summability summable_centred, and the
integrability and nonnegativity inputs. This module composes them once with the abstract branch
splitting primal_branches.
The per-scale family is
avg n w = M_0^{1/2} · ((X)_{z + U_{t-n}} − (X)_{U_t}), the transported recentring of the parent
optimizer field X = (∇v, b ∇v). On 1 < M the whole series is absorbed by the older-scale
term; on M ≤ 1 only the scales beyond a window H are absorbed and the first H + 1 scales
remain as an explicit head sum.
The two older-scale branches of the cell-average estimate at the carriers. For an
invertible selected grid, a generation t, a parent harmonic optimizer attached to the recentred
response coefficient, and the pointwise elliptic data of the parent and normalized blocks, the
normalized seminorm of the recentred transported optimizer field obeys the bad-branch bound
16 / (1 - Quenched.contrastRho γ) · K · √M · ℰ when 1 < M and the good-branch bound
∑_{n ≤ H} 3 ^ (-(n / 2)) S n + 16 / (1 - Quenched.contrastRho γ) · K · 3 ^ (-(Quenched.contrastAlpha γ H)) · ℰ when
M ≤ 1, where K = √(‖(Ehat_t^-)_+‖), ℰ is the weak optimizer energy, and S n is the
depth-n scale average.
HC bridge II: the diagonal weak-norm primal bound (Lemma 2.16) #
The scale-average seminorm and the positive-definiteness facts the bound rests on are developed
in ScaleAverageSeminorm.lean; the supporting defect, energy-map and head estimates are in
DiagonalDefectCarriers.lean, RecentEnergyMapSupport.lean and RecentHeadDefectHalves.lean.
Paper p.response.transfer.
AK.HC Lemma 2.16 on the selected grid, pathwise (the weak-norm kernel). #
The carriers of the weak-norm kernel are the defect carriers and closed helpers of
DiagonalDefectCarriers.lean. Paper p.response.transfer.
The right-hand side below is the explicit printed bound: the finite recent-scale defect sums
16 * K * L * (weakCellSum + weakAverageSum) together with the older-scale energy term
16 / (1 - rho) * K * (if 1 < M then sqrt M else 3 ^ (-(alpha * H))) * E, where
K = sqrt (blockSpecBound (normalizedBlock (respEhatMinus P jStar F t) (respM0 F))),
L = sqrt (respLsqMinus P jStar F t e), E = weakOptimizerEnergy (respCell jStar F t) (respCoeffMinus F a) u and M = respAllScaleMax P γ jStar F t a. The constants are explicit,
and the bound carries the two finite sums rather than a single unspecified universal constant.
SPECIALIZATION. The general (rho, s, delta) bound is specialised here to AK.HC Lemma 2.16
"with exponent 1/2, decay exponent rho, cutoff delta = 1, and window H"
(p.response.transfer), i.e. s = 1/2, rho = Quenched.contrastRho γ = (1+γ)/2, delta = 1.
The side conditions under _hγ : γ ∈ Set.Ico 0 1 hold:
0 < rho:rho = (1+γ)/2 ≥ 1/2 > 0✓rho < 2:γ < 1givesrho < 1 < 2✓rho/2 < s:(1+γ)/4 < 1/2 ⇔ γ < 1✓ (it is exactlyγ < 1)s ≤ 1:1/2 ≤ 1✓0 < delta,delta ≤ 1:delta = 1✓ Two consequent simplifications are performed in the printed constants:(Real.sqrt delta)⁻¹ = (Real.sqrt 1)⁻¹ = 1, and2*s - rho = 1 - Quenched.contrastRho γ(= (1-γ)/2 = 2 * Quenched.contrastAlpha γ > 0). Alsos - rho/2 = 1/2 - (1+γ)/4 = (1-γ)/4 = Quenched.contrastAlpha γ, which is why the tail weight is printed as3^{-(Quenched.contrastAlpha γ * H)}.
CARRIER MAP (paper ↦ current):
adaptedWeakSeminorm q t (1/2) F ↦ besovSeminorm t (cellAverageFamily q t F)— real-valued; the statement is therefore an inequality inℝ, not inℝ≥0∞, and the outerENNReal.ofRealon both sides disappears.diagonalWeakMaximum rho q t E a ↦ respAllScaleMax P γ jStar F t a(ResponseBlockObjects.lean) — REAL-valued, so theif … = ⊤ then ⊤ else …case distinction is unnecessary: there is no⊤branch to state, andrespAllScaleMax …is the real cutoff value.diagonalWeakMetricFactor m E ↦ Real.sqrt (blockSpecBound (normalizedBlock (respEhatMinus P jStar F t) (respM0 F)))— theK₀ofp.response.transfer. The paper's(S, m)binders (S*S = m,Ssymmetric) are absorbed intorespM0 FandblockSqrt, so noS/mbinders are added.diagonalWeakLoadMinus E p r ↦ Real.sqrt (respLsqMinus P jStar F t e)(ResponseBlockObjects.lean) — the loads(p, r)are the response coordinates ofe, so nop rbinders are added.diagonalWeakCellDefect q (t-n) t ↦ weakCellDefect q t n,diagonalWeakAverageDefect ↦ weakAverageDefect,diagonalWeakCellSum ↦ weakCellSum,diagonalWeakAverageSum ↦ weakAverageSum,diagonalWeakEnergy ↦ weakOptimizerEnergy— the five carriers above (blockSize ↦ blockSpecBound ∘ normalizedBlock,avsumspelled out,variationEnergyValueonoptimizerField).diagonalWeakState hq t a p r - blockCellAverage (adaptedCell q t) … ↦the LEFT-hand side (cellAverageFamily … - cellAverage (respCell jStar F t) …). The right-hand side carries the explicit constants16and16 * (√delta)⁻¹ / (2s - rho), printed here.
AK.HC Lemma 2.16 on the selected grid, pathwise: the scale-average seminorm of
the recentred doubled optimizer state is bounded by the two finite recent-scale sums plus the
older-scale energy term, at s = 1/2, rho = Quenched.contrastRho γ and delta = 1; see the
section docstring for the carrier map.
The binder hgrid : IsUnit (respGrid jStar F) supplies the invertibility that
cellAverage_optimizerField_eq_blockResponseMean needs, and the two defect sums take the
recentred field respCoeffMinus F a so that numerator and denominator are congruenced alike; the
two defect carriers use the two-sided norm, the one-sided version being false (see their
docstrings).