BoundarySplit #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The boundary Caccioppoli's `L²` object, split #

BoundaryOuterAssembly.exists_boundaryWindowEnergy_le_dirichletDatumRHS reads its L² object on the covering cube, in that cube's own frame:

  ‖u(·+c) − v‖²_{L²(□_{n+2})} ,   c = wellPlacedCentre x m (n+2) ,

where v is the Dirichlet solution on □_{n+2} carrying the transported boundary datum h(·+c). The frozen right-hand side prices nothing of that shape, so the object must be split against the two zero-trace data the boundary lane actually holds:

  u(·+c) − v  =  (u − h)(·+c)  −  (v − h(·+c)) ,
                 ↑ H¹₀(□_m)               ↑ H¹₀(□_{n+2}) by construction

the second summand is an H¹₀(□_{n+2}) datum, so the Dirichlet Poincaré applies at the cube's own scale.

The Dirichlet leg is proved here from the proved zero-set core rather than imported from CoarseGraining: the zero extension of an H¹₀(□_{n+2}) datum to the enclosing cube □_{n+3} vanishes on the upper slab {½·3^{n+2} ≤ yᵢ}, which the proved three-translate covering shows carries at least a third of □_{n+3}.

What this module does not do. It does not price the second leg's gradient: the output keeps the honest coordinate sum Σᵢ ‖∂ᵢσ‖.

References #

ABK26, l.harmonic.approximation.good.scales, Step 2; l.coarse.grained.Caccioppoli.RHS.

1. The origin cube as an axis cube #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.openCubeSet_originCube_eq_axisCube {d : ℕ} (j : ℤ) :

HCPolySupport.openCubeSet (HCPolySupport.originCube d j) = HCPolySupport.axisCube (fun (x : Fin d) => -(1 / 2) * 3 ^ j) (3 ^ j)

An origin triadic cube is its own lower-corner axis cube.

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.openCubeSet_originCube_subset_axisCube_succ {d : ℕ} (j : ℤ) :

HCPolySupport.openCubeSet (HCPolySupport.originCube d j) ⊆ HCPolySupport.axisCube (fun (x : Fin d) => -(1 / 2) * 3 ^ (j + 1)) (3 ^ (j + 1))

The origin cube sits inside its triadic parent, in the axis realization.

2. The upper slab of the parent cube #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_axisCube_succ_le_three_mul_upperSlab {d : ℕ} (j : ℤ) (i : Fin d) :

MeasureTheory.volume (HCPolySupport.axisCube (fun (x : Fin d) => -(1 / 2) * 3 ^ (j + 1)) (3 ^ (j + 1))) ≤ 3 * MeasureTheory.volume (HCPolySupport.axisCube (fun (x : Fin d) => -(1 / 2) * 3 ^ (j + 1)) (3 ^ (j + 1)) ∩ {y : HCPolySupport.Vec d | 1 / 2 * 3 ^ j ≤ y i})

The parent's upper slab carries a third of the parent.

The level ½·3^j — the upper face of the child □_j — cuts the parent cube □_{j+1} so that the part above it is at least a third of the parent. Landed volume_le_three_mul_slab at lo = -½·3^{j+1}, hi = ½·3^{j+1}, a = ½·3^j, where a − 2(hi − a) = lo exactly.

3. The Dirichlet Poincaré on an origin cube #

source

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.dirichletCubePoincareConst (d : ℕ) :

ℝ

The coefficient-free constant of the Dirichlet Poincaré on an origin triadic cube: 3(1 + √3) times the d-only mean-zero constant of the unit corner cube.

Equations