RebaseSealDistanceErrorWeighted #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The error-weighted seal distance — the boundary instance, and nothing #
else #
RebaseJoinErrorWeighted returns the frozen block from the whole general clause at
the re-gated funding line and the clause event; RebaseGeneralClauseRegated discharges
that clause at frontier-empty windows — the anchor's own interior gate.
Composing them, the remaining caller obligation is exactly the boundary
instance: the same real-valued statement with the gate negated,
(z + □_{n+2}) ∩ ∂□_m ≠ ∅ .
This module performs the composition and the two ε back-ports: the case split
is on the gate, which depends only on d, z, n, m — data bound before the
almost-sure quantifier — so it happens outside the ∀ᵐ and no measurability
question arises. The gate is still the n+2 one: the two re-gated literals are
the funding line and the general clause's threshold, not the interior clause's
trigger.
References #
- ABK26,
l.harmonic.approximation.good.scales; the frozen block ofAlgsuperdiff/Section4/Provider/ExcessDecay/ProviderEpsFree.lean(read for the byte-verification, never imported).
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.exists_harmonicApproximation_provider_of_boundaryClauseReal_errorWeighted
(d : ℕ)
(hbdry :
∃ (C : ℝ),
0 < C ∧ ∀ (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 * (C⁻¹ * s ^ 4) →
∀ (hs : 0 < s) (L m n : ℤ),
m ≤ L →
n + 3 ≤ m →
∀ (x z : HCPolySupport.Vec d),
x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) →
z ∈ 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) →
(fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ frontier (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, ⋯⟩
(C⁻¹ * s ^ 4) →
∀
(u h :
HCPolySupport.H1Function
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(g : HCPolySupport.Vec d → HCPolySupport.Vec d),
Support.IsDirichletSolutionOn
(Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField
(HCPolySupport.originCube d m) u h 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 h.grad) 2
(Support.normalizedGagliardoMeasureOn
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) →
∀
(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 ≤ C * (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 (-(3 / 2)) * Real.rpow 3 ↑n * ‖HCPolySupport.volumeAverageVec
((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet
(HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet
(HCPolySupport.originCube d m))
h.grad‖) + s.rpow (-7) * (↑(Section3.Annealed.sigmaBar M n))⁻¹ * 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 h.grad).toReal + s.rpow (-6) * Support.fluxCorrectedErrorRepresentative M L (n + 3)
⟨s / 8, ⋯⟩
(Section3.Cutoff.translateCutoffSample z omega) * Real.rpow 3 ↑n * (MeasureTheory.eLpNorm h.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))
:
∃ (C : ℝ),
0 < C ∧ ∀ (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 * (C⁻¹ * s ^ 4) →
∀ (hs : 0 < s) (L m n : ℤ),
m ≤ L →
n + 3 ≤ m →
∀ (x z : HCPolySupport.Vec d),
x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) →
z ∈ 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), ∀
(u h :
HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(g : HCPolySupport.Vec d → HCPolySupport.Vec d),
Support.IsDirichletSolutionOn
(Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField
(HCPolySupport.originCube d m) u h 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 h.grad) 2
(Support.normalizedGagliardoMeasureOn
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) →
∀
(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) →
(Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z
⟨s / 8, ⋯⟩ (C⁻¹ * s ^ 4)).indicator
(fun (_omega' : Section3.Cutoff.CutoffSample d) =>
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))))
omega ≤ ENNReal.ofReal
(C * 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))) + ENNReal.ofReal
(s.rpow (-(3 / 2)) * Real.rpow 3 ↑n * ‖HCPolySupport.volumeAverageVec
((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet
(HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet
(HCPolySupport.originCube d m))
h.grad‖)) + ENNReal.ofReal
(C * s.rpow (-7) * (↑(Section3.Annealed.sigmaBar M n))⁻¹ * 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 + ENNReal.ofReal (C * 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 h.grad + ENNReal.ofReal
(C * s.rpow (-6) * Support.fluxCorrectedErrorRepresentative M L (n + 3)
⟨s / 8, ⋯⟩
(Section3.Cutoff.translateCutoffSample z omega) * Real.rpow 3 ↑n) * MeasureTheory.eLpNorm h.grad 2
(Support.normalizedVolumeMeasureOn
((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet
(HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ∧ ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ frontier
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) = ∅ →
(Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d)
(n + 2) z ⟨s / 8, ⋯⟩ (1 / 2)).indicator
(fun (_omega' : Section3.Cutoff.CutoffSample d) =>
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))))
omega ≤ ENNReal.ofReal
(C * s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 2)
⟨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 + 2)) ∩ HCPolySupport.openCubeSet
(HCPolySupport.originCube d m))
u.toFun)
2
(Support.normalizedVolumeMeasureOn
((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet
(HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet
(HCPolySupport.originCube d m))) + ENNReal.ofReal
(C * s.rpow (-(19 / 2)) * (↑(Section3.Annealed.sigmaBar M n))⁻¹ * Real.rpow 3 ((1 + s) * ↑n)) * Support.normalizedGagliardoESeminormOn
((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet
(HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
s g)
The frozen block from the boundary instance alone.
The hypothesis hbdry is the general clause in real form, restricted to
the boundary regime (z+□_{n+2}) ∩ ∂□_m ≠ ∅; the frontier-empty regime is
supplied by exists_generalClauseReal_frontierEmpty_regated, and the ℝ≥0∞ shell,
the join and the interior clause by
exists_harmonicApproximation_provider_of_generalClauseReal_regated.