SealComparator #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Δ-harmonic comparator with the Dirichlet-principle L² bound #
What is proved #
For a translated triadic cube V = translateSet c □_j inside the anchor's
domain □_m and an ambient datum h : H¹(□_m), there is a Δ-harmonic
comparator w ∈ h + H¹₀(V) — the H¹₀ corrector ρ is exposed, with exact
pointwise value and gradient identities — satisfying the coefficient-free
Dirichlet-principle bound (exists_deltaComparator_translatedCube)
‖h − w‖_{L²(V)} ≤ comparatorPoincareConst d · 3^j · Σᵢ ‖∂ᵢh‖_{L²(V)} ,
comparatorPoincareConst d = √d · dirichletCubePoincareConst d, a function of
d alone. The two moves:
- energy minimality (
setIntegral_vecNormSq_grad_corrector_le): testing the corrector's zero-trace weak equation at the identity background with the corrector itself and completing the square gives∫_V |∇ρ|² ≤ ∫_V |∇h|²— no Cauchy–Schwarz on the pairing, no ellipticity constant; - the Dirichlet Poincaré (
BoundarySplit), transported to the translated frame throughH10Function.untranslateand the exact norm transport ofCh01.volumeAverage_translateSet_eq_comp_addRight.
References #
- ABK26,
l.harmonic.approximation.good.scales, Step 2, (the twoΔ-harmonic replacements of the boundary covering argument).
1. L² product integrability and the vecDot expansion #
2. The identity-background corrector #
The zero-trace corrector at the identity background exists: an H¹₀(V)
function ρ with ∫_V ∇ρ·∇φ = −∫_V ∇Φ·∇φ for every φ ∈ H¹₀(V). This is
CoarseGraining's Dirichlet existence theorem at the identity coefficient field.
3. Energy minimality: the Dirichlet principle, by completing the square #
The corrector's gradient energy is at most the datum's.
Test the corrector's own weak equation with the corrector and complete the
square: 0 ≤ ∫|∇Φ + ∇ρ|² = ∫|∇Φ|² − ∫|∇ρ|².
4. The componentwise form of energy minimality #
The componentwise Dirichlet principle.
Σᵢ ‖∂ᵢρ‖_{L²(V)} ≤ √d · Σᵢ ‖∂ᵢΦ‖_{L²(V)} for the identity-background
corrector ρ of the datum Φ.
5. The Dirichlet Poincaré on a translated cube #
The Dirichlet Poincaré on a translated origin cube.
An H¹₀(translateSet c □_j) function obeys the un-subtracted L² Poincaré at
the cube's own scale, with the coefficient-free constant of
BoundarySplit.
6. The packaged comparator #
The comparator's coefficient-free constant: √d times the Dirichlet
Poincaré constant.
Equations
Instances For
The Δ-harmonic comparator on a translated cube, with the
Dirichlet-principle bound.
For V = translateSet c □_j ⊆ □_m and an ambient h : H¹(□_m) there are
w : H¹(V) and an H¹₀(V) corrector ρ with w = h + ρ pointwise (values
and gradients), w weakly Δ-harmonic on V, and
‖h − w‖_{L²(V)} ≤ comparatorPoincareConst d · 3^j · Σᵢ ‖∂ᵢh‖_{L²(V)} .