AssemblyComposedErrorWeighted #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary branch of the error-weighted general clause, composed #
This module is AssemblyComposed's script with ONE row of the regrouping
changed. It does not import AssemblyComposed, which is untouched and still
consumed by the frontier-empty chains, and it claims no anchor.
What is proved #
ReindexComposed composes the deterministic x-frame envelope with the
interior Caccioppoli and proves the general clause at frontier-empty
windows. This module runs the same composition with the boundary energy
leg (AssemblyEnergyLeg) in place of the interior one, and therefore needs
no gate at all: the boundary display is proved for every z, the frontier
condition entering nowhere.
The s-powers, as consumed #
row 1 direct DirE ∇h s^{-4}·(s/2)^{-1/2} → ≤ 2 s^{-6} (legs 4,5)
row 2 direct DirE [g] s^{-4}·(s/2)^{-3/2} → ≤ 3 s^{-7} (force leg)
row 3 datum, crude leg s^{-4}·s^{-1/2} → ≤ s^{-6} (flat leg)
row 4 datum, force leg s^{-4}·(s/2)^{-3} = 8 s^{-7} (force leg)
row 5 datum → DirE [g] s^{-4}·(s/2)^{-3/2}·(s/2)^{-3/2} = 8 s^{-7} (force leg)
row 6 datum → DirE ∇h s^{-4}·(s/2)^{-3/2}·(s/2)^{-1/2} = 4 s^{-6} (legs 4,5)
Row 6 proves at equality: AssemblyArith.pin_gradh_prod supplies the exact
identity (s/2)^{-3/2}·(s/2)^{-1/2} = 4 s^{-2}, so no slack remains on that
row.
References #
- ABK26,
l.harmonic.approximation.good.scales; the boundary application.
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundaryClauseComposed_honest_errorWeighted
(d : ℕ)
[NeZero d]
:
∃ (C : ℝ) (Cfin : ℝ),
0 < C ∧ 0 < Cfin ∧ ∀ (M : Section3.ABKModel d),
∀ s ∈ Set.Icc (64 * M.gamma) 1,
M.gamma ≤ C⁻¹ * 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 →
∀
(v :
HCPolySupport.H1Function
((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))
(w :
HCPolySupport.H10Function
((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))),
Support.IsWeaklyHarmonicOn
((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))
v →
(∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun y - w.toFun y) →
(∀ (y : HCPolySupport.Vec d), v.grad y = u.grad y - w.grad y) →
(MeasureTheory.eLpNorm
(fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2
(Support.normalizedVolumeMeasureOn
((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet
(HCPolySupport.originCube d n)))).toReal ≤ Cfin * (s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 3)
⟨s / 8, ⋯⟩
(Section3.Cutoff.translateCutoffSample z omega) * (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.rpow (-7) * (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * Real.rpow 3 ((1 + s) * ↑n) * (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 (-6) * Real.rpow 3 ((1 + s) * ↑n) * (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 (-6) * Support.fluxCorrectedErrorRepresentative M L (n + 3)
⟨s / 8, ⋯⟩
(Section3.Cutoff.translateCutoffSample z omega) * Real.rpow 3 ↑n * (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 + s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 3)
⟨s / 8, ⋯⟩
(Section3.Cutoff.translateCutoffSample z omega) * S)
The boundary branch of the error-weighted general clause, composed.
The deterministic x-frame envelope with the boundary energy leg substituted:
no frontier condition is used, so the display holds at every z.