ToLambdas #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: comparing the homogenization error with the ellipticity constants #
This file proves a local version of the lower half of Lemma
l.mathcal.E.to.Lambdas of
ABK26:
For every
m ∈ ℤ,q ∈ [1,∞],s ∈ (0,∞), coefficient fieldaand scalarσ₀ ∈ (0,∞),(1/2) 𝓔_{s,∞,q}(□_m; a, σ₀)² ≤ max{σ₀^{-1} Λ_{s,q}(□_m;a), σ₀ λ_{s,q}^{-1}(□_m;a)} ≤ 1 + 2 𝓔_{s,∞,q}(□_m;a,σ₀)² + 2^{1/2} 𝓔_{s,∞,q}(□_m;a,σ₀), and moreover, in the caseq = 2,1 + (1/2) 𝓔_{s,∞,2}(□_m;a,σ₀)² ≤ max{σ₀^{-1} Λ_{s,2}(□_m;a), σ₀ λ_{s,2}^{-1}(□_m;a)}.
Scope #
Proved here, for q = 2:
- the sharp one-cube estimate behind the second inequality of the printed
e.J.by.f, namelymax_{|e|=1} J(U, A₀^{-1/2}e, A₀^{1/2}e; a) ≤ σ₀^{-1}|b(U;a)| + σ₀|σ_*^{-1}(U;a)| - 2for the scalar comparatora₀ = σ₀ Id; - its geometric aggregation
𝓔_{s,∞,2}² + 2 ≤ σ₀^{-1} Λ_{s,2} + σ₀ λ_{s,2}^{-1}; - the display
e.bound.Lambdas.by.Es.q2, and the first inequality ofe.bound.Lambdas.by.Es, both atq = 2.
Not proved here: the second inequality of e.bound.Lambdas.by.Es (the
upper bound max{…} ≤ 1 + 2𝓔² + 2^{1/2}𝓔), whose printed proof runs
through the operator inequalities e.xminusonetimesxminusonesquared.sstar
and e.xminusonetimesxminusonesquared.b and an eigenvector analysis of
f(x) = x^{-1}(x-1)^2; and the aggregation for general q ∈ [1,∞], whose
printed "triangle inequality" step is Minkowski's inequality in L^{q/2}
and is available in that direction only for q ≥ 2.
Main results #
normalizedBlockResponseMax_scalarMatrix_le_weightedCoarseEllipticity_sub_twohomogenizationErrorOnCube_infinity_two_sq_add_two_le_weightedEllipticityone_add_half_homogenizationErrorOnCube_infinity_two_sq_le_max_weightedEllipticity(the displaye.bound.Lambdas.by.Es.q2)half_homogenizationErrorOnCube_infinity_two_sq_le_max_weightedEllipticity(the first inequality ofe.bound.Lambdas.by.Esatq = 2)
References #
- ABK26.
Suprema over finite sets #
A value of f on a finite set is below the finsetSupReal supremum.
The doubled response with scalar normalizers #
Reflecting the second half of the normalized probe flips exactly the
off-diagonal contributions to the doubled response, so the two responses add up
to the diagonal quadratic form of b(U;a) and σ_*^{-1}(U;a).
This is the block-algebra content of the printed identity e.J.by.f for a
scalar comparator, written with the scaling parameter c (which will be
σ₀^{1/2}).
The sharp one-cube bound of e.J.by.f (ABK26) for a scalar comparator: the
normalized doubled response of a unit probe is bounded by the σ₀-weighted
coarse ellipticity norms, minus 2.
The one-cube estimate for the public normalized response #
Coordinates of the scalar inverse-square-root normalizer.
Coordinates of the scalar square-root normalizer.
The positive scalar comparator maps its inverse-root normalized probe to its root normalized probe, for every doubled vector.
The reflected scalar comparator maps the root normalized probe back to its inverse-root normalized probe, for every doubled vector.
The squared Euclidean norm of a doubled vector splits into the two halves.
The one-cube estimate: for the scalar comparator σ Id, the normalized
block-response maximum is bounded by the weighted coarse ellipticity norms minus
2. This is the sharp form of the second inequality of e.J.by.f (ABK26).
Descendant-scale form of the one-cube estimate.
Aggregation at q = 2 #
The geometric aggregation of the one-cube estimate: 𝓔_{s,∞,2}² + 2 is
bounded by the σ₀-weighted sum of the two coarse ellipticity constants. This
is the content of the first inequality of e.bound.Lambdas.by.Es (ABK26) at q = 2.
The display e.bound.Lambdas.by.Es.q2 (ABK26).
The first inequality of e.bound.Lambdas.by.Es (ABK26) at q = 2.