BoundaryAssemblyEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary-regime Caccioppoli display, with the ∇h legs #
l.coarse.grained.Caccioppoli.RHS: with v the Dirichlet solution carrying the
same force and the same boundary datum, the difference u - v has global zero
trace, solves the homogeneous equation, and CoarseGraining's zero-datum theorem
applies to it (exists_boundaryCaccioppoliEnergy_ofDifference). Three steps
separated that from the printed display; this module proves all three and
closes it.
E_core(∇u) ≤ 2 E_core(∇(u-v)) + 2 E_core(∇v) (i) Minkowski
E_core(∇v) ≤ 18^d · E_{□_m}(∇v) (ii) volume ratio
E_{□_m}(∇v) ≤ (Dirichlet energy RHS)² (iv) e.cg.RHS
Step (iv) is CoarseGraining's energyConsequencesRHSTheory, whose right-hand
side dirichletEnergyWithRHSRHS carries both printed legs: the force leg [g]_{B^r}
and the boundary leg ‖∇h‖_{B^r} at dirichletBoundaryGradientField v = ∇h.
That is where the anchor's ∇h terms enter, and it is the whole point of the
boundary lane.
The constant, honestly #
The right-hand side proved here is CoarseGraining's own
dirichletEnergyWithRHSRHS squared, times 2 · 18^d, not the printed normalization
t^{-3} Λ_t ‖∇h‖²_{H^{2t}(□_0)}. No exponent has been moved: the two legs
are CoarseGraining's, at CoarseGraining's exponent r ∈ (0,1) (kept free and
separate from the Caccioppoli pair s, t, since the two CoarseGraining
theorems do not share a normalizer), and the geometric loss 18^d and the
Minkowski factor 2 are explicit. The printed t^{-3}Λ_t shape would require
CoarseGraining's energy theorem restated at the Caccioppoli normalizer, which
is not available and is not attempted.
References #
- ABK26,
l.coarse.grained.Caccioppoli.RHS.
1. The quadratic-form Minkowski step #
The Minkowski step of the printed display.
On the Caccioppoli core the coefficient energy of u is at most twice the
energy of u - v plus twice the energy of v. This is the quadratic-form
triangle inequality ‖σ^{1/2}∇u‖² ≤ 2‖σ^{1/2}∇(u-v)‖² + 2‖σ^{1/2}∇v‖², with
CoarseGraining's own decomposition lemma doing the work.
2. The core-volume ratio #
The core-volume ratio. A core average of the nonnegative coefficient
energy density is at most 18^d = 2^d 3^{2d} times the parent-cube average:
|□_m| / |caccioppoliCoreSet □_m x| ≤ 2^d 3^{2d} for x ∈ □_m.
3. The parent energy is the square of CoarseGraining's energy norm #
The ∇h leg, as an energy bound on the parent cube. CoarseGraining's
Dirichlet energy estimate with right-hand side, squared: its right-hand side
carries the force leg [g] and the boundary leg ‖∇h‖.