EdAssemblyAnchorErrorWeighted

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

The error-weighted anchor at the one-step window choice

The flat ∇h leg

The general clause's flat ∇h leg is the print's own average form, 𝓔-multiplied at the general clause's own flux-corrected-error slot (index n+3, subtype s/8, sample τ_z ω — the first bracket's factor verbatim):

   ofReal( C s^{-6} · 𝓔_{n+3}(τ_z ω) · 3^n · ‖(∇h)_{(z+□_{n+2})∩□_m}‖ ) .

Read at the excess-decay lane's window choice (anchor index n-2) this is C s^{-6} · 𝓔_{n-2+3} · 3^{n-2} · ‖(∇h)_{(z+□_{n-2+2})∩□_m}‖, which is exactly what edLeg_four_le_errorWeighted consumes — at the anchor's own subterms, no repackaging.

The discard that is NOT taken

The print's own step replaces 𝓔 1_𝒢 by C(d) ε. That is the single monotone move that loses the 𝓔 factor, and it is declined throughout this provider chain: 𝓔 is only ever bounded downstream (𝓔 ≤ ε_j), never inverted.

What the expansion costs, and what it saves

That leg is a bare ofReal, with no ℝ≥0∞ carrier of its own. So the shell atoms change shape — ofReal c₁ * (X + ofReal b) + ofReal c₂ * Y + ofReal c₃ * Z + ofReal c₄ instead of the four-carrier form — and the finiteness slot needs three finite carriers instead of four: the ∇h L² MemLp obligation of the unweighted anchor is gone, because a real number's ofReal is finite outright.

References

• ABK26, l.harmonic.approximation.good.scales, (the anchor); l.excess.decay.good.scales, and its proof's window-choice and harmonic-approximation steps; the 𝓔-multiplied slot and the declined discard.

1. The shell atoms

theorem Algsuperdiff.Section4.Provider.ExcessDecay.toReal_ofReal_mul_bracket_add_two_add_flat_le {c₁ b c₂ c₃ c₄ : ℝ} (X Y Z : ENNReal) (hc₁ : 0 ≤ c₁) (hb : 0 ≤ b) (hc₂ : 0 ≤ c₂) (hc₃ : 0 ≤ c₃) (hc₄ : 0 ≤ c₄) : (ENNReal.ofReal c₁ * (X + ENNReal.ofReal b) + ENNReal.ofReal c₂ * Y + ENNReal.ofReal c₃ * Z + ENNReal.ofReal c₄).toReal ≤ c₁ * (X.toReal + b) + c₂ * Y.toReal + c₃ * Z.toReal + c₄

The B.toReal expansion of the general clause's display.

Unconditional — .toReal is multiplicative and subadditive outright, so a ⊤ carrier only collapses the left-hand side to 0.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ofReal_mul_bracket_add_two_add_flat_ne_top {c₁ b c₂ c₃ c₄ : ℝ} {X Y Z : ENNReal} (hX : X ≠ ⊤) (hY : Y ≠ ⊤) (hZ : Z ≠ ⊤) : ENNReal.ofReal c₁ * (X + ENNReal.ofReal b) + ENNReal.ofReal c₂ * Y + ENNReal.ofReal c₃ * Z + ENNReal.ofReal c₄ ≠ ⊤

The hB slot of the one-step consumers, at this shell. There is no ∇h L² carrier: the flat ∇h leg is a bare ofReal, finite outright.

2. The anchor at the one-step window choice

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_oneStepAnchorBound_errorWeighted (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (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) (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), ∀ (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) → ∃ (B : ENNReal), B ≠ ⊤ ∧ (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (C⁻¹ * s ^ 4)).indicator (fun (_omega' : Section3.Cutoff.CutoffSample d) => MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))))) omega ≤ B ∧ B.toReal ≤ 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) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2 + 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 - 2 + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + s.rpow (-(3 / 2)) * 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‖) + 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‖

The harmonic-approximation anchor, applied at the one-step window choice.

The harmonic-approximation anchor bound re-run at the error-weighted statement. For a.e. ω, every Dirichlet datum on □_m and every harmonic replacement on the moved cube y + □_{n-2}, the general clause is available as a finite bound B on the (unchanged) gated indicator, together with the expansion of B.toReal into the four printed legs — the fourth of which is the 𝓔-multiplied flat ∇h average, at the anchor's own subterms. The 𝓔 1_𝒢 ≤ C discard is declined.