Shared boundary assembly constants

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.assemblyBoundaryConstants (d : ℕ) [inst : NeZero d] : ∃ (CE : ℝ) (_ : 0 < CE) (_ : ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ CE⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ (hs : 0 < s) (n : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (L : ℤ), n + 3 ≤ L → Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) ≤ CE * (1 / 2)) (CB : ℝ) (KE : ℝ) (_ : 0 < CB) (_ : ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ CB⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ (hs : 0 < s) (L m n : ℤ), m ≤ L → n + 3 ≤ m → ∀ (x z : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → (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) → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (S : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → |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 → ∀ (hsubx : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), HCPolySupport.Book.Ch03.h1EnergyNormOnCube (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 3) x z omega) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsubx)) ≤ KE * (√↑(Section3.Annealed.sigmaBar M (n + 3)) * Real.rpow 3 (-↑(n + 2)) * (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 + √↑(Section3.Annealed.sigmaBar M (n + 3)) * Real.rpow 3 (-↑(n + 2)) * S + s.rpow (-3) * √(↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * Real.rpow 3 (s * ↑(n + 2)) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal + s.rpow (-2) * √↑(Section3.Annealed.sigmaBar M (n + 3)) * Real.rpow 3 (s * ↑(n + 2)) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s hdat.grad).toReal + s.rpow (-2) * √↑(Section3.Annealed.sigmaBar M (n + 3)) * (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)) (_ : 0 ≤ √(192 * ↑d) * 3) (_ : 0 ≤ √(2 * ↑d * ((√(192 * ↑d) * 3 * (CE * (1 / 2))) ^ 2 + 1)) * (√(192 * ↑d) * 3 * (CE * (1 / 2))) + 2 * (2 * ↑d * ((√(192 * ↑d) * 3 * (CE * (1 / 2))) ^ 2 + 1))) (_ : 0 ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d) (_ : 0 ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d * 216 * (√(192 * ↑d) * 3 * KE)) (_ : 0 ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d * 1944 * ((√(2 * ↑d * ((√(192 * ↑d) * 3 * (CE * (1 / 2))) ^ 2 + 1)) * (√(192 * ↑d) * 3 * (CE * (1 / 2))) + 2 * (2 * ↑d * ((√(192 * ↑d) * 3 * (CE * (1 / 2))) ^ 2 + 1))) * (besovGagliardoConstant d * (gagliardoWindowConst d * windowMoveConst d)))) (_ : 0 ≤ interiorCorrectionConst d * (gagliardoWindowConst d * windowMoveConst d)) (_ : 0 ≤ 9 * (CE * (1 / 2)) * (3 * negNormBaseConst d * coarseGrainingP2Const d * 216 * (√(192 * ↑d) * 3 * KE))), 0 ≤ CE * (1 / 2) * (3 * negNormBaseConst d * coarseGrainingP2Const d * 216 * (√(192 * ↑d) * 3 * KE))

Shared constant package for the boundary assembly and its error-weighted variant.