High-contrast homogenization: Entry.Response.Kernel.ResponseWeakEstimateBasics #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The route to the response weak-norm estimate #
This file lays the route to response_weak_estimate (p.response.transfer): it defines the
per-scale Besov term, the recentred and adjoint defect fields, the response constants
respK0SqMinus/Plus, and the pathwise weak energy respWeakEnergyOf, and proves the structural
facts the route needs - that the Besov seminorm is the tsum of its per-scale term, that it is
unaffected by an additive constant, the pathwise bounds on both signs, and the summability of the
centred term. Every statement here besides the final route theorem is an intermediate that later
files may restate or specialize.
The route to response_weak_estimate (p.response.transfer) #
Every statement here except response_weak_estimate_of_route is an intermediate that may be
restated; the final theorem has the same statement as WeakEstimateAssembly.lean and is proved from
the intermediate lemmas.
Notation: K_0^2 = respK0Sq±, (L^±)^2 = respLsq±, M = respAllScaleMax, Q = bigQ,
α = Quenched.contrastAlpha, ρ = Quenched.contrastRho, S_cell = weakCellSum, S_av = weakAverageSum,
ℰ = weakOptimizerEnergy, c_a = respRecentre± (the recentring vector of p.response.transfer).
Chain for one maximizer family u (minus sign; plus is the twin):
3^{-t/2}·[M_0^{1/2}(⟨X_a⟩_{k,z} - Y)] ≤ 3^{-t/2}·[M_0^{1/2}(⟨X_a⟩_{k,z} - ⟨X_a⟩_{U_t})] + |c_a|/(1-3^{-1/2})
by the triangle inequality, the summability of the centred family and the pathwise bound
≤ 16 K_0 L (S_cell + S_av) + (16/(1-ρ)) K_0 T(a) ℰ(a) + |c_a|/(1-3^{-1/2})
(diagonalWeakNorm_primal_le); square, (x+y+z)^2 ≤ 3(x^2+y^2+z^2), integrate:
∫(S_cell+S_av)^2 ≤ D_H η^{1/Q}, T(a)^2 ℰ(a)^2 ≤ 2 L^2 (M^Q + 3^{-2αH}) a.e.
integrated with ∫ M^Q ≤ C_m η and Integrable M^Q,
∫|c_a|^2 ≤ C K_0^2 L^2 η^{2/Q}; finally K_0^2 L^2 ≤ C κ_s and the rpow
algebra give the integrated estimate, and Real.sSup_le gives the final estimate.
Carriers #
The per-family weak energy 3^{-t} ∫ [Besov]^2 dP of one maximizer family u: the generic
element of the sSup set defining respWeakEnergy (ResponseBlockObjects.lean).
Equations
- One or more equations did not get rendered due to their size.
Instances For
K_0^2 = |M_0^{-1/2} Ehat_t^- M_0^{-1/2}| (paper p.response.transfer), minus sign; the
literal
factor of diagonalWeakNorm_primal_le.
Equations
- One or more equations did not get rendered due to their size.
Instances For
K_0^2 for the plus sign.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The recentring vector c_a = M_0^{1/2}(⟨X_a⟩_{U_t} - Y^-) (paper p.response.transfer),
minus sign.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The recentring vector, plus sign.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The recent-cell normalized defect block at depth n, index w: the summand of
weakCellDefect before the norm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Its norm, the summand of weakCellDefect.
Equations
Instances For
The sSup reduction (p.response.transfer) #
0 ≤ W^± unconditionally (Real.sSup_nonneg: every member is
3^{-t} ∫ (…)^2 ≥ 0; the empty/unbounded junk value is 0).
(W^±)^{1/2} ≤ B once every admissible family has energy ≤ B^2
(Real.sSup_le needs no boundedness in ℝ; then Real.sqrt_le_sqrt, Real.sqrt_sq hB).
Local helper: Minkowski for the normalized finite-cell L² length. #
The corresponding declarations in ScaleAverageSeminorm.lean are private and so cannot be
imported across files; these local copies are needed for the triangle inequality of the Besov
seminorm against a constant family.
Recentring the Besov seminorm (p.response.transfer) #
Triangle inequality of the Besov seminorm against a constant family: a constant
c has [c] = 3^{t/2}|c|/(1-3^{-1/2}). Per scale, Minkowski on the flat average
(card_triadicIndexBox for card > 0), then tsum_le_tsum/tsum_add with hA and the
geometric summability of the constant term.
Local helpers for the summability of the centred family. #
The weak seminorm adaptedWeakSeminorm is an ℝ≥0∞-valued tsum, which converges
unconditionally, so summability is automatic there and no separate summable_* lemma is needed.
The route below therefore uses summable_besov_cellAverageFamily (ScaleAverageSeminorm.lean)
applied to the transported, recentred field x ↦ M_0^{1/2}(X x - ⟨X⟩_{U_t}).
The five algebraic helpers mirror the helpers of
DiagonalWeakNormBound.lean, which are private there and so cannot be
imported, with one deliberate difference: cellAverage_blockMatVecMul_sub_const_eq is stated
PER CELL, not as the funext family identity, because the family identity needs integrability of
X on adaptedCellAtCenter q (t-n) w for EVERY w, whereas the optimizer field is only L² on
U_t and so only controls the w in triadicIndexBox d n -- which is all besovTerm sums over.
memVectorL2_matVecMul corresponds to HCPoly/Entry/Response/Core/SkewShearCongruence.lean
(memVectorL2_const_matVecMul, private there); elliptic_respCoeffMinus/Plus from
EllipticRepresentativeInputs.lean (public, but that file is not in this file's import closure),
whose
own source is Annealed.exists_elliptic_representative_adapted
(HCPoly/Entry/Annealed/AdaptedDomainLocality.lean). Together they supply exactly the L² datum
that
the flux slot needs.
L² input #
Summability of the centred family of the optimizer field
(summable_besov_cellAverageFamily; if that lemma already has this shape this is a one-liner,
otherwise derive it from avsum_cellAverageFamily_sq_le and the geometric weight).
The plus twin of the centred-family summability.
The plus twin (diagonalWeakNorm_primal_le is minus only) #
Local helper for the pathwise bound. #
The only algebra the pathwise bound needs beyond diagonalWeakNorm_primal_le,
besovSeminorm_add_const_le and the summability of the centred family:
M(v - Y) = M(v - C) + M(C - Y), i.e. the p.response.transfer recentring of the Besov family
from the
pathwise cell average C = ⟨X_a⟩_{U_t} to the annealed centre Y^±. The same step appears in
ProfileWeakSplit.lean
(normalized_primal_weak_split / profilePrimalWeakRoot_le_randomCentered_add_constant), where
it is carried by blockCellAverage_metricRoot_sub_const_diagonalWeakState; there it is an
ℝ≥0∞ tsum split (ENNReal.tsum_add), here it is besovSeminorm_add_const_le, which is
why the real-valued route needs the centred-family summability and the ℝ≥0∞ route did not.
The pathwise bound relative to Y^± (p.response.transfer) #
For one a: diagonalWeakNorm_primal_le for the centred family, besovSeminorm_add_const_le
with
c = respRecentreMinus, the summability of the centred family, and the linearity
blockMatVecMul M (v - w) = blockMatVecMul M v - blockMatVecMul M w
(cellAverageFamily is rfl the cell average at adaptedCellAtCenter q (t-n) w). The constant
term
is 3^{-t/2} · 3^{t/2}|c|/(1-3^{-1/2}).
The plus twin of the pathwise bound (uses diagonalWeakNorm_primal_plus and
summable_besovTerm_centred_plus).