Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.ExcessDecay.AssemblyEnergyLeg

AssemblyEnergyLeg #

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

1. The Euclidean L² transport of the boundary gradient #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedEuclideanL2_datumGrad_coveringCube_atWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hcov : (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)) (hL2W : MeasureTheory.MemLp F 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hFcube : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => F (y + wellPlacedCentre x m (n + 2))) :
(normalizedEuclideanL2 (HCPolySupport.originCube d (n + 2)) fun (y : HCPolySupport.Vec d) => F (y + wellPlacedCentre x m (n + 2))) ≤ √↑d * 3 ^ d * (MeasureTheory.eLpNorm F 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 datum pricing's crude datum leg, transported onto the anchor window, at hinge (W).

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedEuclideanL2_datumGrad_coveringCube_le_anchorWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hgeom : (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)) (hL2W : MeasureTheory.MemLp F 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hFcube : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => F (y + wellPlacedCentre x m (n + 2))) :
(normalizedEuclideanL2 (HCPolySupport.originCube d (n + 2)) fun (y : HCPolySupport.Vec d) => F (y + wellPlacedCentre x m (n + 2))) ≤ √↑d * 3 ^ d * (MeasureTheory.eLpNorm F 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 datum pricing's crude datum leg, transported onto the anchor's window.

The datum pricing's third leg is the normalized Euclidean L² norm of the transported boundary gradient on the covering cube.

2. Nonnegativity of CoarseGraining's Dirichlet-energy right-hand side #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.dirichletEnergyWithRHSRHS_nonneg {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {C r : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution Q a g) (hC : 0 ≤ C) (hr : 0 < r) (hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q r g) (hh : HCPolySupport.Book.Ch03.ForceBesovRegularity Q r (HCPolySupport.Book.Ch03.dirichletBoundaryGradientField v)) :
0 ≤ HCPolySupport.Book.Ch03.dirichletEnergyWithRHSRHS C Q a r g v

CoarseGraining's dirichletEnergyWith is nonnegative in the theorem range: its two summands are products of a nonnegative constant, an rpow, an ellipticity rpow and a Besov (semi)norm of a ForceBesovRegularity field.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_neg_one_lambdaSq_le_of_lower_cap {l sigma K : ℝ} (hl : 0 < l) (hsigma : 0 < sigma) (hcap : sigma * l⁻¹ ≤ K) :
l.rpow (-1) ≤ K * sigma⁻¹

The lower ellipticity rpow in the form the datum pricing's second leg carries it.

3. The boundary energy leg, priced onto the anchor's legs #

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundaryWindowAndCoveringRegularity (d : ℕ) [NeZero d] (s : ℝ) :
0 < s → ∀ (m n : ℤ) (x z : HCPolySupport.Vec d), s ≤ 1 → n + 2 ≤ m → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), 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))) → MeasureTheory.MemLp hdat.grad 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp u.toFun 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.volume ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) ≠ 0 → MeasureTheory.IsProbabilityMeasure (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp 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))) ∧ MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ∧ MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ∧ 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))) ≠ ⊤ ∧ 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))) ≠ ⊤ ∧ MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)))) ∧ MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)))) ∧ MeasureTheory.MemLp hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)))) ∧ MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)))) ∧ (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) s fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) ∧ (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) (s / 2) fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) ∧ (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) s fun (y : HCPolySupport.Vec d) => hdat.grad (y + wellPlacedCentre x m (n + 2))) ∧ (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) (s / 2) fun (y : HCPolySupport.Vec d) => hdat.grad (y + wellPlacedCentre x m (n + 2))) ∧ HCPolySupport.translateSet (wellPlacedCentre x m (n + 2)) (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

Window and covering-cube regularity from the parent datum's L² hypotheses.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundaryEnergyDisplayComparison (d : ℕ) [NeZero d] (CB1 CB2 : ℝ) :
0 < CB1 → 0 < CB2 → 0 ≤ 3 ^ d → ∀ (M : Section3.ABKModel d) (s : ℝ), 0 < s → ∀ (L m n : ℤ) (x z : HCPolySupport.Vec d), s ≤ 1 → ∀ (omega : Section3.Cutoff.CutoffSample d) (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hsubx : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) (s / 2) fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) → (HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) (s / 2) fun (y : HCPolySupport.Vec d) => hdat.grad (y + wellPlacedCentre x m (n + 2))) → ∀ (v : HCPolySupport.Book.Ch03.DirichletForcedCubeSolution (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))), (∀ (y : HCPolySupport.Vec d), v.boundaryData.grad y = hdat.grad (y + wellPlacedCentre x m (n + 2))) → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((parentRebasedFamily M L (n + 3) x z omega).coeffOn (HCPolySupport.originCube d n)) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsubx)) ≤ 3 ^ d * (2 * (HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor CB1 (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) (1 / 2) (s / 3) * (HCPolySupport.Book.Ch02.lambdaS (HCPolySupport.originCube d (n + 2)) (s / 3) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) * Real.rpow 3 (-2 * ↑(n + 2)) * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun (y + wellPlacedCentre x m (n + 2)) - v.toH1.toFun y)) + 2 * (18 ^ d * HCPolySupport.Book.Ch03.dirichletEnergyWithRHSRHS CB2 (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) (s / 2) (fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) v ^ 2)) → (HCPolySupport.Book.Ch03.dirichletBoundaryGradientField v = fun (y : HCPolySupport.Vec d) => hdat.grad (y + wellPlacedCentre x m (n + 2))) ∧ HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) (s / 2) (HCPolySupport.Book.Ch03.dirichletBoundaryGradientField v) ∧ HCPolySupport.Book.Ch03.h1EnergyNormOnCube (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 3) x z omega) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsubx)) = √(HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((parentRebasedFamily M L (n + 3) x z omega).coeffOn (HCPolySupport.originCube d n)) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsubx))) ∧ 0 ≤ HCPolySupport.Book.Ch02.lambdaS (HCPolySupport.originCube d (n + 2)) (s / 3) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) ∧ √(HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((parentRebasedFamily M L (n + 3) x z omega).coeffOn (HCPolySupport.originCube d n)) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsubx))) ≤ √(2 * 3 ^ d * (HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor CB1 (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) (1 / 2) (s / 3) * HCPolySupport.Book.Ch02.lambdaS (HCPolySupport.originCube d (n + 2)) (s / 3) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega))) * (√(Real.rpow 3 (-2 * ↑(n + 2))) * √(HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun (y + wellPlacedCentre x m (n + 2)) - v.toH1.toFun y)) + √(2 * 3 ^ d * 18 ^ d) * HCPolySupport.Book.Ch03.dirichletEnergyWithRHSRHS CB2 (HCPolySupport.originCube d (n + 2)) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) (s / 2) (fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) v ∧ √(Real.rpow 3 (-2 * ↑(n + 2))) = Real.rpow 3 (-↑(n + 2))

Boundary-gradient identification and square-root bounds for the energy display.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_windowEnergy_boundary_le_anchorLegs_atHinges (d : ℕ) [NeZero d] :
∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (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) => 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 → √(M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage (truncatedWindow x m n) fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad y)) ≤ K * (√↑(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)

Boundary energy on the truncated window under the covering containments.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_h1EnergyNormOnCube_boundary_le_anchorLegs_atHinges (d : ℕ) [NeZero d] :
∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (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) => 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)) ≤ K * (√↑(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)

Cube-energy specialization of the window bound under the covering containments.

source
theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_h1EnergyNormOnCube_boundary_le_anchorLegs (d : ℕ) [NeZero d] :
∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (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 → ∀ (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)) ≤ K * (√↑(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)

The boundary lane's energy leg.

CoarseGraining's coefficient-energy norm on the child cube, at the (n+3) re-based family — the quantity the deterministic x-frame envelope carries inside its energy term — priced onto the five canonical legs of the boundary chain.