EdAssemblyJoinDatumSplitErrorWeighted

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

1. The join at the honest boundary binders, at the error-weighted anchor

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_oneStep_anchored_datumSplit_errorWeighted (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Cb : ℝ), 0 < C ∧ 0 ≤ Cb ∧ ∀ (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), ∀ delta ≤ 1, delta ≤ 64 * (C ^ 2)⁻¹ * s ^ 6 → ∀ (L m n : ℤ), m ≤ L → n - 2 + 3 ≤ m → ∀ (x z : HCPolySupport.Vec d), x ∈ truncatedWindow z m (n - 3) → 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 - 2 + 3) z ⟨s / 8, ⋯⟩ (s / 8 * √delta) → ∀ (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))) → ∀ (v : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))) (w : HCPolySupport.H10Function ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))), Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))) 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) → ∀ (Kh : ℝ), 0 ≤ Kh → ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) ∨ ∃ (i : Fin d) (V : HCPolySupport.Vec d → ℝ) (v₁ : HCPolySupport.Vec d → ℝ) (cl : ℝ) (Al : HCPolySupport.Vec d), (MeetsUpperFace x m (n - 2) i ∨ MeetsLowerFace x m (n - 2) i) ∧ MeasureTheory.MemLp v.toFun 2 (MeasureTheory.volume.restrict (truncatedWindow x m n)) ∧ MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))) ∧ (V =ᵐ[MeasureTheory.volume.restrict (truncatedWindow x m (n - 2))] fun (y : HCPolySupport.Vec d) => v.toFun y - affineLift x cl Al y - v₁ y) ∧ (∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (truncatedWindow x m (n - 2)), |v₁ y| ≤ datumResidualBound d n Kh) ∧ (∀ (l : Fin d), MeetsUpperFace x m (n - 2) l → ∀ y ∈ reflectedWindow x m (n - 2), ⋯) ∧ (∀ (l : Fin d), MeetsLowerFace x m (n - 2) l → ∀ (y : HCPolySupport.Vec d), ⋯) ∧ InnerProductSpace.HarmonicOnNhd (V ∘ ⇑⋯) (⇑Schauder.toEuc '' reflectedWindow x m (n - 2))) → ∀ (k : ℕ), 3 ≤ k → Support.affineExcess (truncatedWindow x m (n - ↑k)) u.toFun ≤ taylorContractionConst d * max (Schauder.schauderWindowConst d) Cb * windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m n) u.toFun + triangleRemainderConst d (max (Schauder.schauderWindowConst d) Cb) k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * (C * s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n - 2 + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * ((MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => ⋯) 2 (Support.normalizedVolumeMeasureOn ⋯)).toReal + s.rpow (-(3 / 2)) * Real.rpow 3 ↑(n - 2) * ‖HCPolySupport.volumeAverageVec ⋯ hdat.grad‖) + C * s.rpow (-7) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ * Real.rpow 3 ((1 + s) * ↑(n - 2)) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2 + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal + C * s.rpow (-6) * Real.rpow 3 ((1 + s) * ↑(n - 2)) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2 + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s hdat.grad).toReal + C * s.rpow (-6) * Support.fluxCorrectedErrorRepresentative M L (n - 2 + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * Real.rpow 3 ↑(n - 2) * ‖HCPolySupport.volumeAverageVec ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2 + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) hdat.grad‖))) + taylorContractionConst d * (3 ^ (n - ↑k)) ^ (1 / 2) * (boundaryDatumLegConst d (max (Schauder.schauderWindowConst d) Cb) k * Kh)

The anchored one-step at every scale-n window, with the printed datum leg, at the error-weighted anchor.

The anchored one-step with the printed datum leg, with the anchor re-pointed at the error-weighted statement: the remainder's B.toReal expansion is the error-weighted five-leg block (the fifth leg the 𝓔-multiplied flat ∇h average), and everything else — the window disjunction, the contraction, the remainder weight and the datum leg — is that theorem's, character for character.