Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.ExcessDecay.CoarseBoundaryClause

CoarseBoundaryClause #

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

The boundary Caccioppoli's parent-L² object, priced onto the frozen legs #

Nothing here imports that file, and nothing here claims the anchor or any source node.

What is proved #

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

priced onto the frozen clause's own legs. In the same-boundary-data architecture the split is a two-term triangle, not the plan's quadrangle:

  ‖u(·+c) − v_cc‖ ≤ ‖u − h‖_{L²(c+□_{n+2})}   +   ‖v_cc − h‖_{L²(□_{n+2})} ,

the second summand being exactly CoarseDatumPricing's output. The first summand is decomposed (§2) as

  ‖u − h‖_{L²(cc)}
      ≤ ‖u − (u)_{cc}‖_{L²(cc)} + |(u−h)_{cc}| + ‖h − (h)_{cc}‖_{L²(cc)}
      ≤ 3^d ‖u − (u)_{W'}‖_{L²(W')}            (mean-minimality + window transport)
        + S                                      (the open scalar, threaded)
        + C(d) 3^{n+2} d 3^d ‖∇h‖_{L²(W')} ,    (data Poincaré on h alone)

See CoarseMeanComparison for the machine-checked record that the mean-comparison chain bounds S by this very quantity rather than the other way round.

References #

1. The coordinate gradient against the ambient gradient #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_grad_coord_le_eLpNorm_grad {d : ℕ} {A : Set (HCPolySupport.Vec d)} (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (i : Fin d) :
MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => G y i) 2 (Support.normalizedVolumeMeasureOn A) ≤ MeasureTheory.eLpNorm G 2 (Support.normalizedVolumeMeasureOn A)

A coordinate of the gradient is dominated by the ambient (sup) norm, in the normalized L² carrier.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.sum_toReal_eLpNorm_grad_coord_le {d : ℕ} {A : Set (HCPolySupport.Vec d)} (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (hfin : MeasureTheory.eLpNorm G 2 (Support.normalizedVolumeMeasureOn A) ≠ ⊤) :
∑ i : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => G y i) 2 (Support.normalizedVolumeMeasureOn A)).toReal ≤ ↑d * (MeasureTheory.eLpNorm G 2 (Support.normalizedVolumeMeasureOn A)).toReal

The coordinate sum of the datum gradient is at most d times the ambient one.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.toReal_eLpNorm_coveringCube_atWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} (hcov : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {f : HCPolySupport.Vec d → ℝ} (hfin : MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) :
(MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))).toReal ≤ 3 ^ d * (MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal

2. The covering-cube pricing of ‖u − h‖, at the hinge #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coveringCube_sub_datum_le_meanControl_atWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {S : ℝ} (hnm : n + 2 ≤ m) (hcov : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hXfin : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hHfin : MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hmean : |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y| ≤ S) :
(Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y) ≤ 3 ^ d * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + S + HCPolySupport.unitMeanZeroPoincareConst d * 3 ^ (n + 2) * (↑d * (3 ^ d * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal))

The three legs of the parent-L² pricing, at the hinge.

The re-cut of normalizedL2On_coveringCube_sub_datum_le_meanControl: on the boundary covering cube the L² distance between the solution and its own boundary datum is priced by the frozen clause's leg (mean-minimality and the window transport of section 1), the frozen leg (the proved data Poincaré on h alone), and the open scalar S = |(u−h)_{cc}| at coefficient 1.

2. The covering-cube pricing of ‖u − h‖, modulo the scalar #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coveringCube_sub_datum_le_meanControl {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {S : ℝ} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hXfin : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hHfin : MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hmean : |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y| ≤ S) :
(Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y) ≤ 3 ^ d * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + S + HCPolySupport.unitMeanZeroPoincareConst d * 3 ^ (n + 2) * (↑d * (3 ^ d * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal))

The three legs of the parent-L² pricing.

On the boundary covering cube cc = c + □_{n+2} the L² distance between the solution and its own boundary datum is priced by two of the frozen clause's own legs — one through mean-minimality and the window transport, the other through the proved data Poincaré on h alone — and the open scalar S = |(u−h)_{cc}| at coefficient 1.

hmean is a conditional A obligation (the mean-comparison bound); every other input is the anchor's own data.

3. The two-term split of the Caccioppoli's parent-L² object #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_openCubeSet_eq_cubeLpNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (HCPolySupport.openCubeSet Q))) :
Support.normalizedL2On (HCPolySupport.openCubeSet Q) f = HCPolySupport.cubeLpNorm Q 2 f

The normalized L² seminorm on an open cube is the cube L² norm.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_sub_dirichletSolution_le_split {d : ℕ} (Q : HCPolySupport.TriadicCube d) {a : HCPolySupport.Book.Ch03.CoeffFamily d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution Q a g) (utr : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) :
(Support.normalizedL2On (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => utr.toFun y - v.toH1.toFun y) ≤ (Support.normalizedL2On (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => utr.toFun y - v.boundaryData.toFun y) + HCPolySupport.cubeLpNorm Q 2 fun (y : HCPolySupport.Vec d) => v.toH1.toFun y - v.boundaryData.toFun y

The same-boundary-data split.

For CoarseGraining's DirichletForcedCubeSolution v on Q and any H¹ competitor utr on Q, the object the boundary Caccioppoli puts on its right-hand side splits into the datum distance and the datum pricing's zero-trace leg:

  ‖utr − v‖_{L²(Q)} ≤ ‖utr − h‖_{L²(Q)} + ‖v − h‖_{L²(Q)} .

Nothing is subtracted through the operator: h is v's own boundary datum and the force is g on both sides.

4. The composed parent-L² pricing, modulo the scalar S #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coveringDifference_le_meanControl_atWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {S : ℝ} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hcov : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution (HCPolySupport.originCube d (n + 2)) a g) (utr : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)))) (hutr : ∀ (y : HCPolySupport.Vec d), utr.toFun y = u.toFun (y + wellPlacedCentre x m (n + 2))) (hvdat : ∀ (y : HCPolySupport.Vec d), v.boundaryData.toFun y = hdat.toFun (y + wellPlacedCentre x m (n + 2))) (hXfin : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hHfin : MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hmean : |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y| ≤ S) :
√(HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => utr.toFun y - v.toH1.toFun y) ≤ 3 ^ d * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + S + HCPolySupport.unitMeanZeroPoincareConst d * 3 ^ (n + 2) * (↑d * (3 ^ d * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal)) + HCPolySupport.cubeLpNorm (HCPolySupport.originCube d (n + 2)) 2 fun (y : HCPolySupport.Vec d) => v.toH1.toFun y - v.boundaryData.toFun y

The parent-L² pricing, composed, at the hinge.

The re-cut of normalizedL2On_coveringDifference_le_meanControl: the boundary Caccioppoli's parent-L² object at the covering cube, priced onto the frozen legs and the datum pricing's zero-trace leg, with the open scalar S threaded additively at coefficient 1.

3. The scaled parent-L² object, at the hinge #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coveringDifference_le_meanControl {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {S : ℝ} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution (HCPolySupport.originCube d (n + 2)) a g) (utr : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)))) (hutr : ∀ (y : HCPolySupport.Vec d), utr.toFun y = u.toFun (y + wellPlacedCentre x m (n + 2))) (hvdat : ∀ (y : HCPolySupport.Vec d), v.boundaryData.toFun y = hdat.toFun (y + wellPlacedCentre x m (n + 2))) (hXfin : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hHfin : MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≠ ⊤) (hmean : |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y| ≤ S) :
√(HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => utr.toFun y - v.toH1.toFun y) ≤ 3 ^ d * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + S + HCPolySupport.unitMeanZeroPoincareConst d * 3 ^ (n + 2) * (↑d * (3 ^ d * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal)) + HCPolySupport.cubeLpNorm (HCPolySupport.originCube d (n + 2)) 2 fun (y : HCPolySupport.Vec d) => v.toH1.toFun y - v.boundaryData.toFun y

The parent-L² pricing, composed.

The boundary Caccioppoli's parent-L² object at the covering cube, priced onto the frozen legs and the datum pricing's zero-trace leg, with the open scalar S threaded additively at coefficient 1:

  ‖u(·+c) − v_cc‖_{L²(□_{n+2})}
      ≤ 3^d ‖u − (u)_{W'}‖_{L²(W')}
        + S
        + C_P(d) 3^{n+2} d 3^d ‖∇h‖_{L²(W')}
        + ‖v_cc − h‖_{L²(□_{n+2})} .

hutr and hvdat are exactly the two frame identities BoundaryEnergyRebase's proof already carries (utr = u(·+c) by rfl, v.boundaryData = h(·+c) by its own conclusion).