SuperposedCoordinateConclusion

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

A finite-coordinate reduction of the corrected superposed A

The operator-norm consumers of Section 3 do not require an almost-sure bound simultaneous over the uncountable unit sphere. Positivity bounds each of the two coarse matrix norms by its trace, and both traces are sums of the 2 * d pure coordinate quadratic forms

((sqrt sigma)\u207b\u00b9 e_j, 0),    (0, sqrt sigma e_j).

The deterministic theorem below records that reduction using CoarseGraining's trace A. The final theorem intersects the corrected superposed conclusion only over j : Fin d, once for each pure leg. It retains the exact scale-separation, wave-envelope, and all-load potential gates; no gate is strengthened and no uncountable intersection is taken.

Deterministic finite-coordinate trace reduction

The exact superposed payload at one load

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.superposedConclusionPayload {d : ℕ} (M : ABKModel d) (m i L : ℤ) (E b eps t beta : ℝ) (k₀ kp : ℕ) (omega : Cutoff.CutoffSample d) (p q : HCPolySupport.Vec d) : ℝ

The right-hand side of the corrected assembled superposed conclusion at one unframed load (p,q).

Equations

• One or more equations did not get rendered due to their size.

A simultaneous a.e. result over exactly 2 * d loads