SeriesEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The energy estimate on a cube, and the Dirichlet problem for a perturbed coefficient field #
The C^{0,1/2} contraction of the Section 5.1 iteration says nothing about the
H¹ size of its iterates, and a Hölder bound alone cannot identify a limit as a
weak solution. What identifies it is the energy estimate
lam ‖∇u‖_{L²(y+□_n)} ≤ d ‖g‖_{L²(y+□_n)}
for -∇·a∇u = ∇·g with zero boundary values: the antisymmetric part of a
drops out when the equation is tested with the solution itself, so only the
lower ellipticity constant survives. The dimensional factor d is the price of
the supremum-norm carrier, paid once in abs_setIntegral_vecDot_le.
This module collects that estimate together with the algebra a perturbed
coefficient field needs. If b = a + kap pointwise and both fields are
elliptic on the cube, then a solution for a at forcing G is a solution for
b at forcing G - kap ∇u; the perturbation kap is automatically bounded
entrywise by the sum of the two upper ellipticity constants, and its action on
an L² field is again L² because it is the difference of the actions of b
and of a. No separate regularity or boundedness hypothesis on kap is
required.
Main results #
sqrt_energy_grad_le_of_isDirichletSolutionAt— the energy estimate.sqrt_setIntegral_sq_le_of_sup_bound— theL²size of a field from its supremum size on the cube.sqrt_setIntegral_sq_matVecMul_le— theL²size of the action of an entrywise bounded matrix field.isDirichletSolutionAt_add— additivity of the localized Dirichlet problem.isDirichletSolutionAt_coeff_add— the same solution read against the perturbed coefficient field.
References #
- ABK26, the localized Dirichlet problems of Section 5.1.
1. Elementary L² bookkeeping #
The energy integral of a field is nonnegative.
The L² size of a field from its supremum size on a set of finite
volume.
2. Matrix algebra on the ambient carrier #
The action of a matrix field is additive in the matrix.
The action of a matrix field is subtractive in the matrix.
The L² size of the action of an entrywise bounded matrix field.
3. The energy estimate #
The energy estimate for the localized Dirichlet problem. Testing
-∇·a∇u = ∇·g with the solution itself and using only the lower ellipticity
constant gives
lam ‖∇u‖_{L²(y+□_n)} ≤ d ‖g‖_{L²(y+□_n)} .
The antisymmetric part of a contributes nothing: the hypothesis used is the
one-sided bound lam |ξ|² ≤ ξ·aξ, which a skew addition to a leaves
untouched.
4. Additivity of the localized Dirichlet problem #
The sum of two solutions solves the problem for the sum of the forcing fields.
5. The perturbed coefficient field #
The perturbation between two fields elliptic on the cube is bounded entrywise by the sum of their upper ellipticity constants.
The sum of the two upper ellipticity constants is nonnegative.
The action of the perturbation on an L² field is again L²: it is the
difference of the actions of the two elliptic fields.
A solution for a is a solution for b = a + kap at the forcing field
corrected by the action of the perturbation on its own gradient.