HarmonicReplacement #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Harmonic-replacement well-posedness: the constant-coefficient Dirichlet replacement #
Nothing here imports that file, and nothing here claims the anchor or any source node.
What is built #
ABK26's Step 1 introduces two constant-coefficient comparison functions on the
child window W = x+□_n:
-Δ v = 0 in W , v = u on ∂W;
-σ Δ v_g = ∇·g in W , v_g = u on ∂W .
This module produces both, and their uniqueness, from CoarseGraining.
exists_isZeroTraceDirichletRhsWeakSolution_of_potentialZeroTraceClosureRealization
(a := a) (U := U) (g := G) …
: ∃ v : H10Function U, IsZeroTraceDirichletRhsWeakSolution a U v G
(PDE.exists_isZeroTraceDirichletRhsWeakSolution_of_potentialZeroTraceClosureRealization),
an H¹₀(U) weak solution of −∇·a∇ρ = ∇·G for any G ∈ L²(U) and any
elliptic field a, together with its defining identity and the uniqueness
statements
IsZeroTraceDirichletRhsWeakSolution.gradToVectorL2_eq_of_isEllipticFieldOn
and .toScalarL2_eq_of_isOpenBoundedConvexDomain. The closure-realization
hypothesis is discharged on an open cube by
hasPotentialZeroTraceClosureRealization_of_isOpenBoundedConvexDomain.
Nothing had to be reinvented: the whole content of this module is the affine
shift v = u − ρ that converts the zero-trace problem into the u-trace
problem, by moving the datum's own flux a₀∇u into the forcing.
The construction #
For u ∈ H¹(W) and g ∈ L²(W;ℝ^d) put
correctorForce a₀ u g := a₀∇u − g ∈ L²(W;ℝ^d) ,
let ρ be the H¹₀(W) solution of −∇·a₀∇ρ = ∇·(a₀∇u − g), and set
v := u − ρ. Then −∇·a₀∇v = ∇·g weakly and u − v = ρ ∈ H¹₀(W) on the
nose (not merely a.e.), which is what the downstream coarse-graining datum and
the H¹₀ test function of the negative-norm-to-L² step both need.
harmonicReplacement is the same object at g = 0; since a₀ = σ Id is
scalar, −∇·a₀∇v = 0 is −Δv = 0, the printed equation.
References #
- ABK26,
l.harmonic.approximation.good.scales.
1. Domain facts for the open triadic cube #
The open triadic cube carries the abstract zero-trace potential closure realization CoarseGraining's Dirichlet existence theorem asks for.
A constant coefficient matrix is an elliptic field on the open cube.
2. Splitting a forcing pairing #
The forcing pairing is additive in the force, in the form the affine shift produces it (the combined field is given pointwise).
The forcing pairing is subtractive in the force.
3. The corrector force #
The force of the zero-trace problem solved by the correction u − v: the
datum's own constant-coefficient flux a₀∇u minus the printed force g.
Equations
- Algsuperdiff.Section4.Provider.ExcessDecay.correctorForce a0 u g x = HCPolySupport.matVecMul a0.matrix (u.grad x) - g x
Instances For
The constant-coefficient flux of an H¹ function is square integrable.
The corrector force is square integrable whenever the printed force is.
4. The chosen H¹₀ corrector #
Existence of the zero-trace corrector. This is CoarseGraining's Dirichlet existence theorem, specialized to the constant background on the open cube.
The chosen zero-trace corrector. The H¹₀(W) weak solution of
−∇·a₀∇ρ = ∇·(a₀∇u − g).
Equations
Instances For
5. The forced replacement v_g and the harmonic replacement v #
The auxiliary forced solution v_g of tex e.harmonic.approx.v.def.with.g:
the element u − ρ of u + H¹₀(W) solving −∇·a₀∇v_g = ∇·g weakly.
Equations
Instances For
The zero-trace difference is exact. u − v_g = ρ pointwise, with ρ
the chosen H¹₀ corrector; in particular v_g ∈ u + H¹₀(W).
The gradient of the exact zero-trace difference.
v_g solves the printed constant-coefficient forced problem.
The affine shift, read backwards: if u − w solves the forced problem for
an H¹₀ function w, then w solves the zero-trace problem for the corrector
force.
Uniqueness of the replacement, value form. This is the exact sense in which the printed "the unique solution of the Dirichlet problem" is realized.