StepSevenFlushWindowEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
theorem
Algsuperdiff.Section4.Provider.Regularity.ae_windowEnergy_flush_S_killed
(d : ℕ)
[NeZero d]
:
∃ (C : ℝ) (A : ℝ) (K1 : ℝ) (K2 : ℝ),
0 < C ∧ 0 < A ∧ 0 < K1 ∧ 0 ≤ K2 ∧ ∀ (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) (sigma : ℝ),
sigma = 1 ∨ sigma = -1 →
ExcessDecay.wellPlacedHalfGap m (n + 2) < sigma * 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) →
A * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩
(Section3.Cutoff.translateCutoffSample z omega) ≤ s ^ 4 →
∀
(u hdat :
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 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))) →
√(M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage
(ExcessDecay.truncatedWindow z m n)
fun (y : HCPolySupport.Vec d) =>
HCPolySupport.vecNormSq (u.grad y)) ≤ K1 * (√↑(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)) * (K2 * ((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 + 3 ^ n * ∑ i' : Fin d,
(MeasureTheory.eLpNorm
(fun (y : HCPolySupport.Vec d) =>
hdat.grad y i')
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 (-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 (-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 (-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 (-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)
The flush-branch window energy, S-free.
At every centre z ∈ □_m with the flush-direction overhang at the covering
scale n+2, almost surely on the good event at (n+3, z), under the ε-pin,
the Step-7 window scalar √ν‖∇u‖_{(z+□_n)∩□_m} is priced on the window's own
legs — the oscillation leg, the datum legs and the forcing legs — with NO
normalization scalar. unit 5 composed with's priced scalar.