ShellWindowEnergyCentre

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

1. The two covering inclusions at the diagonal

theorem Algsuperdiff.Section4.Provider.Regularity.translateSet_cubeSet_coveringCube_subset_anchorParent_of_sub {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hw : x - z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1))) : HCPolySupport.translateSet (ExcessDecay.wellPlacedCentre x m (n + 2) - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2))) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3))

The covering cube inside the n+3 parent, half-open, off the displacement datum. BoundaryCoveringSlot.translateSet_cubeSet_coveringCube_subset_anchorParent with its geometry binder replaced by the only consequence its proof uses.

theorem Algsuperdiff.Section4.Provider.Regularity.translateSet_cubeSet_coveringCube_subset_anchorParent_self {d : ℕ} {n m : ℤ} {z : HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : HCPolySupport.translateSet (ExcessDecay.wellPlacedCentre z m (n + 2) - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2))) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3))

The covering inclusion at the diagonal. At x = z the displacement datum is 0 ∈ □_{n+1}, so the half-open containment holds for centre of □_m.

theorem Algsuperdiff.Section4.Provider.Regularity.image_add_wellPlacedCentre_subset_anchorWindow_self {d : ℕ} {n m : ℤ} {z : HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : (fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z 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)

The clamped outer cube inside the anchor window, at the diagonal. StepSevenCaccBoundaryGate.image_add_wellPlacedCentre_subset_truncatedWindow_succ at j = n+2, with the scale normalized.

2. The boundary energy leg at every centre

theorem Algsuperdiff.Section4.Provider.Regularity.ae_windowEnergy_boundary_le_anchorLegs_atCentre (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 → ∀ z ∈ 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) => ExcessDecay.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 → √(M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage (ExcessDecay.truncatedWindow z 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)

The boundary lane's energy leg at the anchor's own window centre.

unit 4 with its two covering-geometry hypotheses discharged at the diagonal x = z. There is no geometry binder left: interior, boundary centres are all covered.