GammaTenStripTransfer

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

Signed boundary transfer on recurrence meshes

The earlier LocalizationFluctuationMeshTransfer module proves the signed finite-grid transfer under its original Closure name and derives the nonnegative estimate from it. This module combines that shared transfer with the recurrence's boundary count, retaining arbitrary real families and the scale bookkeeping K = n + p, outer + 1 = n + g, g ≤ p.

The Step-2 fluctuation integrand is a difference of energies and can have either sign. The signed transfer uses the nonnegative part of its interior average.

References

• ABK26, l.approximate.recurrence.formula Step 2, e.lower.bound.localization.terms, e.recurrence.params.

The signed split at the recurrence's own two meshes

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_mesoCubeGrid_le_max_interior_add (d : ℕ) {K n outer : ℤ} {p g : ℕ} (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) (F : HCPolySupport.TriadicCube d → ℝ) : cubeFamilyAverage (mesoCubeGrid d K n) F ≤ max (cubeFamilyAverage (interiorMesoCubeGrid d K n outer) F) 0 + √(↑d * (3 ^ g / 3 ^ p)) * √(cubeFamilyAverage (mesoCubeGrid d K n) fun (R : HCPolySupport.TriadicCube d) => F R ^ 2)

The signed boundary split on the mesh.

The full-mesh average of an arbitrary real family is below the truncated interior average plus sqrt(d 3^{g-p}) times the square root of the full-mesh average of its square. The signed mirror of LocalizationFluctuationMeshTransfer.gridFourthMoment_mesoCubeGrid_le_interior_add.

only on the scale bookkeeping.