ResidueRouteOne #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Route 1, machine-assembled at the flush sub-cube K' #
Nothing here imports that file, and nothing here claims the anchor or any source node.
What is proved #
derived, from the shapes of the proved theorems, that the p = 2
coarse-graining comparison read at the flush scale-n sub-cube K' = flushSubCentre z m n i σ + □_n prices the harmonic-approximation residue ‖u − w‖_{L²(K')} on the five canonical legs, but could not assemble it, because
the proved caps carry the anchor's geometry binder and K' provably fails it.
This module is that assembly:
‖u − w‖_{L²(K')} ≤ Cfin ·
( s^{-4}·𝓔·‖u − (u)_{W'}‖_{L²(W')}
+ s^{-7}·σ_{n+3}^{-1}·3^{(1+s)n}·[g]_{H^s(W')}
+ s^{-6}·3^{(1+s)n}·[∇h]_{H^s(W')}
+ s^{-6}·3^{n}·‖∇h‖_{L²(W')}
+ s^{-4}·𝓔·S )
with 𝓔 = fluxCorrectedErrorRepresentative M L (n+3) ⟨s/8⟩ (translate z ω)
carried explicitly (not substituted by the frozen good event's ε = 1/2),
and S the boundary scalar at the flush cube K = wellPlacedCentre z m (n+2) + □_{n+2} — which is the covering cube of K'
(ResidueCapGeometry.wellPlacedCentre_flushSubCentre).
- the deterministic
x-frame envelopeReindexEllipticity.eLpNorm_sub_weaklyHarmonic_le_coarseGraining_rebased_addThree(binder-free: it needs onlytranslateSet x □_n ⊆ □_m); - the boundary energy leg at the two hinges (
ResidueEnergyLeg); - the child cube's
𝓔-cap and forcing bracket at hinge (C) (ResidueCapChild); - the one-hop Gagliardo transport
K' → W'(ResidueFlushTransport) in place of the proved two-hop route through the(n+2)window, whichK'does not meet.
The σ-cancellation, machine-verified #
The envelope is divided by σ₀ = σ_{n+3} and the energy term carries
‖a₀‖^{1/2} = √σ_{n+3} (constantCoeffMatrixNormHalf_scalarComparator_sqrt).
The two identities √σ·√σ = σ and √σ·√(σ^{-1}) = 1 are consumed at h1 and h2
below: they cancel σ exactly on the four √σ legs and leave exactly one
σ^{-1} on the force leg. No ν is divided anywhere: CoarseGraining's
h1EnergyNormOnCube at the re-based family equals √(ν·⨍|∇u|²), and that
quantity is consumed whole by the boundary energy leg — it is never converted
to a Euclidean gradient.
References #
- ABK26,
l.harmonic.approximation.good.scales; the boundary application;e.homogenization.L2.interior.
@[reducible, inline]
Child-cube geometry and transport facts shared by the two boundary routes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
The energy comparison contract shared by the two boundary routes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.residueRouteOne_comparisonBounds5
(d : ℕ)
[NeZero d]
(CE KE : ℝ)
:
have kappa := √(192 * ↑d) * 3;
have e0 := kappa * (CE * (1 / 2));
have k0 := 2 * ↑d * (e0 ^ 2 + 1);
have b0 := √k0 * e0 + 2 * k0;
have cg := 3 * negNormBaseConst d * coarseGrainingP2Const d;
∀ (M : Section3.ABKModel d) (s : ℝ) (x : 0 < s) (L m n : ℤ) (z : HCPolySupport.Vec d) (i : Fin d) (sigma : ℝ)
(omega : Section3.Cutoff.CutoffSample d)
(u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(g : HCPolySupport.Vec d → HCPolySupport.Vec d) (S : ℝ)
(v :
HCPolySupport.H1Function
((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i sigma + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))
(hsubx :
HCPolySupport.translateSet (flushSubCentre z m n i sigma)
(HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆
HCPolySupport.openCubeSet (HCPolySupport.originCube d m)),
have Erep :=
Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega);
have sig := ↑(Section3.Annealed.sigmaBar M (n + 3));
0 < sig →
0 ≤ sig⁻¹ →
have X :=
(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;
have Gs :=
(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;
have Hs :=
(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;
have Hn :=
(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;
have Ychild :=
(Support.normalizedGagliardoESeminormOn
((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i sigma + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))
s g).toReal;
Ychild ≤ flushWindowConst d * Gs →
have Lhs :=
(MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2
(Support.normalizedVolumeMeasureOn
((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i sigma + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))).toReal;
have P2 := Real.rpow 3 (-↑(n + 2));
have Q3s := Real.rpow 3 (s * ↑(n + 2));
have Q3sn := Real.rpow 3 (s * ↑n);
0 ≤ Q3sn →
have R3n := Real.rpow 3 ↑n;
0 ≤ R3n →
have Sm3 := s.rpow (-3);
have Sm2 := s.rpow (-2);
have ET :=
coarseGrainingEnergyTerm (HCPolySupport.originCube d n)
(parentRebasedFamily M L (n + 3) (flushSubCentre z m n i sigma) z omega) (scalarComparator ⋯) (s / 3)
(HCPolySupport.H1Function.untranslate (flushSubCentre z m n i sigma) (u.restrict ⋯ hsubx));
ET ≤ √(192 * ↑d) * 3 * KE * Erep * (↑(Section3.Annealed.sigmaBar M (n + 3)) * (P2 * X) + ↑(Section3.Annealed.sigmaBar M (n + 3)) * (P2 * S) + Sm3 * (Q3s * Gs) + Sm2 * (↑(Section3.Annealed.sigmaBar M (n + 3)) * (Q3s * Hs)) + Sm2 * (↑(Section3.Annealed.sigmaBar M (n + 3)) * Hn)) →
have FT :=
coarseGrainingForceTerm (HCPolySupport.originCube d n)
(parentRebasedFamily M L (n + 3) (flushSubCentre z m n i sigma) z omega) (scalarComparator ⋯) (s / 3)
s fun (y : HCPolySupport.Vec d) => -g (y + flushSubCentre z m n i sigma);
FT ≤ b0 * (besovGagliardoConstant d * Q3sn * (flushWindowConst d * Gs)) →
↑(Section3.Annealed.sigmaBar M (n + 3)) * (Real.rpow 3 (-↑n) * Lhs) ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d * (216 * s⁻¹ ^ 4 * ET + 1944 * s⁻¹ ^ 6 * FT) + interiorCorrectionConst d * s.rpow (-(1 / 2)) * Q3sn * Ychild →
0 ≤ sig⁻¹ * R3n ∧ sig⁻¹ * sig = 1 ∧ Lhs ≤ sig⁻¹ * R3n * (cg * (216 * s⁻¹ ^ 4 * ET + 1944 * s⁻¹ ^ 6 * FT) + interiorCorrectionConst d * s.rpow (-(1 / 2)) * Q3sn * Ychild) ∧ 216 * s⁻¹ ^ 4 * ET ≤ 216 * s⁻¹ ^ 4 * (kappa * KE * Erep * (sig * (P2 * X) + sig * (P2 * S) + Sm3 * (Q3s * Gs) + Sm2 * (sig * (Q3s * Hs)) + Sm2 * (sig * Hn))) ∧ 1944 * s⁻¹ ^ 6 * FT ≤ 1944 * s⁻¹ ^ 6 * (b0 * (besovGagliardoConstant d * Q3sn * (flushWindowConst d * Gs))) ∧ interiorCorrectionConst d * s.rpow (-(1 / 2)) * Q3sn * Ychild ≤ interiorCorrectionConst d * s.rpow (-(1 / 2)) * Q3sn * (flushWindowConst d * Gs)
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.residueRouteOne_comparisonBounds6
(d : ℕ)
[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) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆
(fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) →
HCPolySupport.translateSet (wellPlacedCentre x m (n + 2) - z)
(HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2))) ⊆
HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3)) →
∀ᵐ (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 * flushWindowConst d)))
(_ : 0 ≤ interiorCorrectionConst d * flushWindowConst 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))
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.exists_flushResidue_route1_composed_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 →
∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m),
∀ (i : Fin d) (σ : ℝ),
σ = 1 ∨ σ = -1 →
wellPlacedHalfGap m (n + 2) < σ * z i →
∀ᵐ (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 z 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) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))
(w :
HCPolySupport.H10Function
((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))),
Support.IsWeaklyHarmonicOn
((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + 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) =>
flushSubCentre z m n i σ + 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)
Route 1, composed at the flush sub-cube — the error-weighted legs.
The harmonic-approximation residue at K', priced on the five canonical legs
with the good-event error 𝓔 carried explicitly. As in AssemblyComposedErrorWeighted,
the monotone discard is declined on the flat ∇h row, so that leg reads
s^{-6}·𝓔·3^n·‖∇h‖_{L²(W')}.
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.exists_flushResidue_route1_composed
(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 →
∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m),
∀ (i : Fin d) (σ : ℝ),
σ = 1 ∨ σ = -1 →
wellPlacedHalfGap m (n + 2) < σ * z i →
∀ᵐ (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 z 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) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))
(w :
HCPolySupport.H10Function
((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))),
Support.IsWeaklyHarmonicOn
((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + 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) =>
flushSubCentre z m n i σ + 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) * 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)