CoarseAssemblyDatum

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

Boundary Caccioppoli with the full boundary datum

The cube estimate specializes the shared window theorem and retains the value and gradient identities of the comparison solution's boundary data.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundaryWindowEnergy_rebased_le_dirichletDatumRHS_full (d : ℕ) [NeZero d] : ∃ (C₁ : ℝ) (C₂ : ℝ), 0 < C₁ ∧ 0 < C₂ ∧ ∀ (M : Section3.ABKModel d) (L : ℤ) (omega : Section3.Cutoff.CutoffSample d) (m n : ℤ) (x z : HCPolySupport.Vec d) (s t r : ℝ) (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n + 2 ≤ m → ∀ (hsubx : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat g → 0 < s → s < 1 → 0 < t → t < 1 / 2 → s + t < 1 → 0 < r → r < 1 → (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) r fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) → (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) r fun (y : HCPolySupport.Vec d) => hdat.grad (y + wellPlacedCentre x m (n + 2))) → ∃ (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))), (∀ (y : HCPolySupport.Vec d), v.boundaryData.toFun y = hdat.toFun (y + wellPlacedCentre x m (n + 2))) ∧ (∀ (y : HCPolySupport.Vec d), v.boundaryData.grad y = hdat.grad (y + wellPlacedCentre x m (n + 2))) ∧ HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((parentRebasedFamily M L (n + 3) x z omega).coeffOn (HCPolySupport.originCube d n)) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsubx)) ≤ 3 ^ d * (2 * (HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C₁ (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) s t * (HCPolySupport.Book.Ch02.lambdaS (HCPolySupport.originCube d (n + 2)) t (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) * Real.rpow 3 (-2 * ↑(n + 2)) * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun (y + wellPlacedCentre x m (n + 2)) - v.toH1.toFun y)) + 2 * (18 ^ d * HCPolySupport.Book.Ch03.dirichletEnergyWithRHSRHS C₂ (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) r (fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) v ^ 2))

The boundary Caccioppoli, with the full datum identity exported.

BoundaryEnergyRebase.exists_boundaryWindowEnergy_rebased_le_dirichletDatum with the produced comparison solution's boundary datum identified with the anchor's transported datum in **both** halves — values and gradients. The gradient half is what the Dirichlet-energy leg needs in order to read dirichletEnergyWith's boundary-gradient leg on ∇h(· + c).