ToLambdasUpper #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the upper half of l.mathcal.E.to.Lambdas at q = 2 #
This file proves a local version of the second inequality in the display
e.bound.Lambdas.by.Es
of ABK26 in the case q = 2:
max{σ₀^{-1} Λ_{s,2}(□_m;a), σ₀ λ_{s,2}^{-1}(□_m;a)} ≤ 1 + 2 𝓔_{s,∞,2}(□_m;a,σ₀)² + 2^{1/2} 𝓔_{s,∞,2}(□_m;a,σ₀).
The lower half is ToLambdas.lean; the two halves are assembled here in
bound_max_weightedEllipticity_by_homogenizationErrorOnCube_infinity_two.
Proof route #
The printed proof runs through the operator inequalities
e.xminusonetimesxminusonesquared.sstar and
e.xminusonetimesxminusonesquared.b, reads off the eigenvalue function
f(x) = x^{-1}(x-1)^2 on an eigenvector of σ₀ σ_*^{-1}(U;a), and optimizes in
ε. Here the same estimate is obtained without any spectral decomposition:
- both printed operator inequalities are equivalent, on each vector
u, to the single scalar statementf(P) ≤ P + R - 2andf(R) ≤ P + R - 2for the two normalized quadratic formsP = σ⁻¹ u·b(U;a)uandR = σ u·σ_*^{-1}(U;a)u, which byinvMulSubOneSq_le_add_sub_twoonly needs1 ≤ P * R; 1 ≤ P * Ris Cauchy--Schwarz for the positive definite formσ_*(U;a)together withσ_*(U;a) ≤ b(U;a)in the Löwner order;P + R - 2 ≤ 2 max_{|e|=1} Jis the first inequality of the printede.J.by.f, obtained here from the reflection identity ofToLambdas.leanat the half-probe(u, 0);- the Euclidean operator norms
|b|and|σ_*^{-1}|are recovered from the quadratic forms because both matrices are positive semidefinite.
Main results #
vecDot_bCoarse_add_vecDot_sigmaStarInvCoarse_sub_two_le(the first inequality ofe.J.by.f, in quadratic-form shape)inv_mul_coarseBMatrixNorm_le_one_add_add_sqrtandmul_coarseSigmaStarInvMatrixNorm_le_one_add_add_sqrt(the sharp one-cube upper bounds)inv_mul_LambdaSq_leandmul_lambdaSq_inv_le(aggregatedε-forms)max_weightedEllipticity_le_one_add_two_mul_sq_add_sqrt_two_mul(the second inequality ofe.bound.Lambdas.by.Esatq = 2)
References #
- ABK26.
Quadratic forms and the Euclidean operator norm #
A quadratic form bounded on the unit sphere is bounded everywhere, by homogeneity.
For a positive semidefinite matrix, a bound for the quadratic form on the unit sphere bounds the Euclidean operator norm.
The product of the two coarse quadratic forms #
Cauchy--Schwarz for the positive definite form σ_*(U;a), combined with the
Löwner bound σ_*(U;a) ≤ b(U;a): the quadratic forms of b(U;a) and
σ_*^{-1}(U;a) have product at least |u|⁴.
This is the vector-level content of the two printed operator inequalities
e.xminusonetimesxminusonesquared.sstar and
e.xminusonetimesxminusonesquared.b (ABK26).
The first inequality of e.J.by.f #
The normalized block-response value set of a scalar comparator is bounded
above, by the one-cube estimate of ToLambdas.lean.
The first inequality of the printed e.J.by.f (ABK26) in quadratic-form
shape: on a unit vector, the σ-weighted sum of the two coarse quadratic forms
minus 2 is at most twice the normalized block-response maximum.
The proof evaluates the reflection identity of ToLambdas.lean at the
half-probe (u, 0), whose reflection is itself.
The sharp one-cube upper bounds #
The sharp one-cube upper bound for σ^{-1} |b(Q;a)|.
The sharp one-cube upper bound for σ |σ_*^{-1}(Q;a)|.
The ε-linearized one-cube and one-scale bounds #
The ε-linearized one-cube bound for σ^{-1} |b(Q;a)| (ABK26).
The ε-linearized one-cube bound for σ |σ_*^{-1}(Q;a)|.
Descendant-scale form of the ε-linearized bound for |b|.
Descendant-scale form of the ε-linearized bound for |σ_*^{-1}|.
Aggregation at q = 2 #
The aggregated ε-linearized bound for σ^{-1} Λ_{s,2}.
The aggregated ε-linearized bound for σ λ_{s,2}^{-1}.
The upper half of e.bound.Lambdas.by.Es at q = 2 #
Nonnegativity of the multiscale homogenization error at p = ∞, q = 2.
The second inequality of e.bound.Lambdas.by.Es (ABK26)
at q = 2:
max{σ^{-1} Λ_{s,2}, σ λ_{s,2}^{-1}} ≤ 1 + 2 𝓔_{s,∞,2}² + 2^{1/2} 𝓔_{s,∞,2}.