BoundaryEnergyRebase

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

The boundary energy estimate, re-based on the parent's (n+3) flux increment

BoundaryOuterAssembly.exists_boundaryWindowEnergy_le_dirichletDatum runs the boundary Caccioppoli at the covering cube's own flux-corrected family wellPlacedFluxCorrectedFamily M L m k x ω. Every coarse-grained cap the frozen general clause supplies — BoundaryPrefactor's ae_coveringCubeCapsPair_le and ae_coveringCubePrefactor_le — is written at the parent-rebased family parentRebasedFamily M L (n+3) c z ω, c = wellPlacedCentre x m (n+2), because that is the family the good event 𝒢(n+3, z; s/8, 1/2) controls. This module re-runs the boundary energy estimate at that family.

No Λ/λ is converted by invariance anywhere in this module (R-ii).

The left-hand side is ν-free

BoundaryOuterAssembly states its conclusion as ν ⨍|∇u|² on the anchor's own window. Here the same quantity is written as CoarseGraining's own localizedCoeffEnergyValue on the child cube □_n at the x-frame re-based family — the object ReindexComposed's chain consumes as h1EnergyNormOnCube² — so that no estimate slot of this module carries ν. Both sides of the transport are ν ⨍|∇u|² on their own window, so ν cancels inside the proof and the inequality is the pure 3^d volume ratio.

References

• ABK26, l.coarse.grained.Caccioppoli; l.harmonic.approximation.good.scales, (the "differ by a constant anti-symmetric matrix" observation).

1. The covering transport at the re-based family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.nu_mul_normalizedSetAverage_truncatedWindow_le_coreEnergy_rebased {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (omega : Section3.Cutoff.CutoffSample d) {m n : ℤ} {x z : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n + 2 ≤ m) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : (M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage (truncatedWindow x m n) fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad y)) ≤ 3 ^ d * HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d (n + 2)) (x - wellPlacedCentre x m (n + 2))) ((parentRebasedFamily M L k (wellPlacedCentre x m (n + 2)) z omega).coeffOn (HCPolySupport.originCube d (n + 2))) (HCPolySupport.H1Function.untranslate (wellPlacedCentre x m (n + 2)) (u.restrict ⋯ ⋯))

The anchor's child-cube energy, transported onto CoarseGraining's Caccioppoli core.

The localized coefficient energy of the x-frame re-based family on the child cube □_n is at most 3^d times the localized coefficient energy of the c-frame re-based family on CoarseGraining's Caccioppoli core of the covering cube, c = wellPlacedCentre x m (n+2).

2. The boundary energy estimate at the re-based family, at the window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundaryWindowEnergy_rebased_window_le_dirichletDatumRHS (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 → 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))) ∧ (M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage (truncatedWindow x m n) fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad y)) ≤ 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-regime energy estimate at the (n+3) re-based family, read at the anchor's own truncated window.

BoundaryEnergyRebase's display with its localizedCoeffEnergyValue (□_n) left-hand side — and the inclusion binder x + □_n ⊆ □_m it requires — replaced by BoundaryOuterAssembly's gate-free ν ⨍_{(x+□_n)∩□_m} |∇u|². The comparison solution v on the covering cube is produced, carrying the transported boundary datum h(·+c).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedCoeffEnergyValue_childCube_le_three_pow_mul_coveringCore {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (omega : Section3.Cutoff.CutoffSample d) {m n : ℤ} {x z : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n + 2 ≤ m) (hsubx : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((parentRebasedFamily M L k x z omega).coeffOn (HCPolySupport.originCube d n)) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsubx)) ≤ 3 ^ d * HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d (n + 2)) (x - wellPlacedCentre x m (n + 2))) ((parentRebasedFamily M L k (wellPlacedCentre x m (n + 2)) z omega).coeffOn (HCPolySupport.originCube d (n + 2))) (HCPolySupport.H1Function.untranslate (wellPlacedCentre x m (n + 2)) (u.restrict ⋯ ⋯))

2. The boundary energy estimate at the re-based family