BlockBesovSeminorm #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The block negative-Besov seminorm on R^{2d}-valued fields #
ABK26 Remark r.cg.poincare.doubled.variables states the coarse-grained
Poincare inequality e.CG.Poincare.doubled.vars for the doubled fields X in S(cu_m). Its left-hand side is a negative Besov seminorm of two
R^{2d}-valued fields, bfA_0^{1/2} X and bfA_0^{-1/2} bfA X, whereas
CoarseGraining only carries the Vec d-valued negative Besov seminorms. This
module supplies the missing block seminorm -- item (alpha) of the
infrastructure list recorded in DoubledEnergyIdentity.lean.
The seminorm choice #
For F : Vec d -> BlockVec d we take the sum of the two Vec d-valued
negative q = 2 seminorms of the two halves,
blockNegativeBesovTwo Q s F
= [F.1]_{B^{-s}_{2,2}(Q)} + [F.2]_{B^{-s}_{2,2}(Q)} .
The display's own left-hand side is already a sum of two block seminorms, and
the sum rendering lets the diagonal bfA_0^{+-1/2} scaling factor out through
Vec d-homogeneity with no combination loss. The Euclidean block seminorm is
dominated by this one (sqrt(a^2+b^2) <= a+b), so any bound proved here is a
bound for it as well.
Main results #
blockNegativeBesovTwo-- the block seminorm, and its nonnegativity.cubeBesovNegativeVectorSeminormTwo_const_smul_add_le/_const_smul_sub_le-- the scaled two-term triangle steps, from the scalar homogeneity chaincubeAverage_const_mul -> cubeAverageVec_const_smul -> cubeBesovNegativeVectorDepthSeminorm_const_smul -> cubeBesovNegativeVectorPartialSeminormTwo_const_smuland CoarseGraining'ssqrt 2-triangle inequality.blockNegativeBesovTwo_doubledState_leandblockNegativeBesovTwo_doubledFlux_le-- the two splits of the display's left-hand side into the four single-variable seminorms.
Scope #
It consumes no anchor, no frozen theorem and no external input, and contains no
sorry.
References #
- ABK26,
r.cg.poincare.doubled.variables, displaye.CG.Poincare.doubled.vars;e.form.of.A.naught;e.bfA.magic.swapping.
Scalar homogeneity of the negative q = 2 Besov seminorm #
cubeAverage is ℝ-linear under a constant scalar factor.
cubeAverageVec commutes with a constant scalar smul.
Depth-j seminorm homogeneity under a nonnegative constant smul.
Finite-depth q = 2 seminorm homogeneity under a nonnegative constant smul.
Lift a finite-depth triangle estimate to a bound by the full seminorms after scaling.
The two scaled triangle steps #
[c (u + v)] <= c sqrt 2 ([u] + [v]): homogeneity pulls c out,
CoarseGraining's sqrt 2-triangle bounds the sum.
[c (u - v)] <= c sqrt 2 ([u] + [v]).
The block seminorm #
The block negative q = 2 Besov seminorm of a BlockVec d-valued field:
the sum of the two Vec d-valued half-seminorms. This is the [. ]_{B^{-s}_{2,2}(Q)} of e.CG.Poincare.doubled.vars.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two splits of e.CG.Poincare.doubled.vars #
The bfA_0^{1/2} X split. With bfA_0 = diag(sigma0, sigma0^{-1})
(e.form.of.A.naught at scalar sigma0 and kappa0 = 0) and
X = (grad v + grad v*, a grad v - a^t grad v*) (e.findSfull),
bfA_0^{1/2} X = (sigma0^{1/2}(grad v + grad v*),
sigma0^{-1/2}(a grad v - a^t grad v*)) ,
and its block seminorm splits into the four single-variable seminorms with the
honest sqrt 2 triangle loss.
The bfA_0^{-1/2} bfA X split. By the swapping identity
e.bfA.magic.swapping,
bfA X = (a grad v + a^t grad v*, grad v - grad v*) ,
so bfA_0^{-1/2} bfA X = (sigma0^{-1/2}(a grad v + a^t grad v*), sigma0^{1/2}(grad v - grad v*)), and its block seminorm splits into the same
four single-variable seminorms.