DoubledCoarsePoincare #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The coarse-grained Poincare inequality in the doubled variables #
ABK26 Remark r.cg.poincare.doubled.variables, display
e.CG.Poincare.doubled.vars: for bfA_0 of the form e.form.of.A.naught with
sigma_0 scalar and kappa_0 = 0, and every X in S(cu_m),
3^{-sm}[bfA_0^{1/2} X]_{B^{-s}_{2,q}} + 3^{-sm}[bfA_0^{-1/2} bfA X]_{B^{-s}_{2,q}}
<= 4 c_{s,q}^{-1/q} ( sigma_0^{1/2} lambda_{s,q}^{-1/2}(cu_m;a)
+ sigma_0^{-1/2} Lambda_{s,q}^{1/2}(cu_m;a) )
|| bfA^{1/2} X ||_{L^2(cu_m)} .
The manuscript calls this "an immediate consequence of
p.coarse.grained.Poincare, the identity e.bfA.magic.swapping and the
characterization e.findSfull". The three implicit ingredients are supplied by
the sibling modules:
BlockBesovSeminorm.lean-- the block seminorm onR^{2d}-valued fields and the two splits of the left-hand side (alpha);DoubledAdjointEllipticity.lean--lambda_{s,q}(Q;a^t) = lambda_{s,q}(Q;a)andLambda_{s,q}(Q;a^t) = Lambda_{s,q}(Q;a), which is what lets the adjoint half of the argument land on the display's primal constants (beta);TruncationPoincareBridge.lean--p.coarse.grained.Poincareatq = 2on the concrete seminorm, together with the truncation bounds that make the supremum form of the triangle inequality available (gamma).
Along e.findSfull the doubled field is
X = (grad v + grad v^*, a grad v - a^t grad v^*) with v a solution of a
and v^* a solution of a^t, and by e.bfA.magic.swapping
bfA X = (a grad v + a^t grad v^*, grad v - grad v^*). Since bfA_0 is the
diagonal diag(sigma_0, sigma_0^{-1}) at scalar sigma_0 and kappa_0 = 0,
its square roots act diagonally, which is the content of doubledStateField
and doubledFluxField below.
The constant #
The manuscript's 4 c_{s,q}^{-1/q} is reached exactly: the two splits each
cost one factor sqrt 2 (CoarseGraining proves the concrete q = 2 triangle
inequality in the sqrt 2 form), so the two block seminorms together cost 2 sqrt 2, and the passage from the sum of the two scalar energies to the doubled
energy costs a further sqrt 2 -- 2 sqrt 2 * sqrt 2 = 4.
Exponent window #
q = 2 throughout, and s in (0,1): the CoarseGraining coarse Poincare
package carries the endpoint side condition s = 1 -> q = 1. Step 2 of
l.approximate.recurrence.formula names s = 1 but discards s to s = gamma < 1 in its next step, so the open window is what is consumed downstream.
Main results #
doubledStateField,doubledFluxField-- the twoR^{2d}-valued fields on the display's left-hand side.doubledMuValue_doubledFieldOfSolutions-- the integrated form ofblockEnergyDensityAt_doubledFieldOfSolutions:mu(X) = ||sigma^{1/2} grad v||^2 + ||sigma^{1/2} grad v^*||^2, so that|| bfA^{1/2} X ||_{L^2(Q)} = sqrt(2 mu(X)).doubledCoarsePoincare_le-- the display with the doubled energy carried as a named premisehenergy.doubledCoarsePoincare_le_doubledEnergy-- the display at the manuscript's own right-hand side,henergydischarged.
References #
- ABK26,
r.cg.poincare.doubled.variables;p.coarse.grained.Poincare;e.bfS;e.findSfull;e.form.of.A.naught;e.bfA.magic.swapping.
The two scaled doubled fields #
bfA_0^{1/2} X along e.findSfull, at bfA_0 = diag(sigma_0, sigma_0^{-1}):
(sigma_0^{1/2}(grad v + grad v^*), sigma_0^{-1/2}(a grad v - a^t grad v^*)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
bfA_0^{-1/2} bfA X, after the swapping identity e.bfA.magic.swapping:
(sigma_0^{-1/2}(a grad v + a^t grad v^*), sigma_0^{1/2}(grad v - grad v^*)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The doubled energy #
|| bfA^{1/2} X ||_{L^2(U)}^2 is twice the mu-value of X, and by the pointwise identity
of DoubledEnergyIdentity.lean that value is the sum of the two scalar
energies. The two lemmas below integrate the pointwise identity and use it to
discharge the doubled-energy premise of the display.
The scalar energy integrand of a Chapter 2 solution is integrable on the
domain: the flux is in L^2 by a.e. ellipticity, and the integrand is the
vecDot of two L^2 fields.
The scalar energy value of a Chapter 2 solution is nonnegative.
The doubled energy of e.findSfull's field is the sum of the two scalar
energies. This is the integrated form of
blockEnergyDensityAt_doubledFieldOfSolutions.
The arithmetic of the display #
The display #
e.CG.Poincare.doubled.vars at q = 2.
For s in (0,1), a scalar sigma_0 > 0, a solution v of a and a solution
v^* of a^t on the cube Q, the two block negative Besov seminorms of
bfA_0^{1/2} X and bfA_0^{-1/2} bfA X are jointly controlled by
4 c_{s,2}^{-1/2} ( sigma_0^{1/2} lambda_{s,2}^{-1/2}(Q;a)
+ sigma_0^{-1/2} Lambda_{s,2}^{1/2}(Q;a) ) * blockE ,
where blockE dominates the sum of the two scalar energies -- the manuscript's
|| bfA^{1/2} X ||_{L^2(Q)} (see the module header).
on hs, hs1, _hsig0 and henergy. _hsig0 is the source's own
positivity of the scalar sigma_0 (e.form.of.A.naught at a scalar matrix);
it is carried because it is what makes bfA_0 the matrix of that display, and
it is inert in the proof, the two diagonal factors entering only through
Real.sqrt sig0 >= 0. Everything else -- the four single-variable Poincare
bounds, the adjoint identification of the two ellipticity constants, the L^2
memberships and the truncation bounds -- is discharged internally.
e.CG.Poincare.doubled.vars at q = 2, with the doubled energy in place.
The premise henergy of doubledCoarsePoincare_le is discharged at the
manuscript's own right-hand side || bfA^{1/2} X ||_{L^2(Q)} = sqrt(2 mu(X)),
so the only remaining binders are the exponent window and the positivity of the
scalar sigma_0.