HarmonicReplaceExistence #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Harmonic replacement, and the energy minimality of the correction #
Let w be an H^1 function on a bounded open convex domain U which solves, in
the weak sense against H^1_0 (U) competitors, a Laplace equation with
divergence-form right-hand side,
int_U <grad w, grad psi> = int_U <G, grad psi> for every psi in H^1_0 (U) .
Subtracting from w the H^1_0 potential phi of the recentred forcing
G - c produces h := w - phi, and the two weak formulations cancel exactly:
the residual pairing is int_U <c, grad psi>, which vanishes because the mean
gradient of a zero-trace function is zero. Thus h is variationally harmonic,
hence -- through HarmonicReplaceBridge -- weakly harmonic in the distributional
sense that the interior Weyl lemma and the oscillation decay consume.
The same solve is energy-minimal: testing the equation for phi against phi
itself gives int |grad phi|^2 = int <G - c, grad phi>, and expanding the
nonnegative square int |(G - c) - grad phi|^2 >= 0 turns that identity into
int_U |grad w - grad h|^2 = int_U |grad phi|^2 <= int_U |G - c|^2 ,
for every constant c. Dividing by |U| states it as a comparison of
normalized mean squares, which is the shape the oscillation telescope consumes:
the deviation of the correction is bounded by the deviation of the forcing from
an arbitrary constant, in particular from its own average.
No Cauchy-Schwarz inequality and no Poincare inequality is used; the argument is the completed square only.
Contents #
vecDot_sub_left',vecNormSq_sub_eq-- the pointwise algebra of the completed square in the coordinate inner product.isOpenBoundedConvexDomain_openCubeAtScale-- the concentric cubes of the oscillation family belong to the domain class of the solve.exists_h10Function_isWeaklyHarmonicOn_sub-- the harmonic replacement, with the energy bound, on an abstract bounded open convex domain.exists_h10Function_isWeaklyHarmonicOn_sub_openCubeAtScale-- the same on a concentric cube, with the energy bound in normalized mean-square form.
Portability #
This file depends only on Mathlib, on CoarseGraining
(Homogenization.*) and on the harmonic layer of this same directory. It
mentions no object of the manuscript: no model, no cutoff, no shell, no
corrector, no sigmaBar. It is intended to be portable into CoarseGraining by
a single mechanical namespace rename.
References #
- ABK26,
e.nablaw.oscillations(the eventual consumer).
Left additivity of the coordinate inner product in subtracted form.
The completed square in the coordinate inner product.
The concentric cube z + cu_m is a bounded open convex domain, hence a legal
domain for the Laplace-Dirichlet solve.
Harmonic replacement with energy minimality.
Let w be an H^1 function on a nonempty bounded open convex domain U which
weakly solves - Delta w = div G against H^1_0 (U) competitors, and let c be
an arbitrary constant vector. Then there is phi in H^1_0 (U) such that
w - phiis weakly harmonic onUin the distributional sense ofHarmonicWeak, andint_U |grad phi|^2 <= int_U |G - c|^2.
The first conclusion is the cancellation of the two weak formulations, using that a constant pairs to zero with the gradient of a zero-trace function; the second is the completed square.
Harmonic replacement on a concentric cube, in normalized mean-square form.
The specialization of the previous theorem to U = z + cu_m, with the energy
bound divided by the volume of the cube so that both sides are the normalized
mean squares that the oscillation telescope compares. Taking c to be the
average of G on the cube turns the right-hand side into
meanSquareOscillationVecOn (z + cu_m) G, which is the quantity the birth-scale
forcing atom of OscillationApproxForcing bounds.