GoodLocalEventAtBridge

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

The centred presentation of the good local event

The frozen event goodLocalEventAt M Ccg m n z is the pullback of the centred good local event at scale m by translation of the cutoff sample through z. For a triadic cube Q, taking m = Q.scale and z = triadicCubeShift Q recovers exactly the existing cube-indexed event goodLocalEvent M Ccg Q n.

The sign is positive on the sample translation: translateCutoffSample z evaluates each shell at x + z, which turns the centred cube into the cube whose base point is z.

theorem Algsuperdiff.Section3.Provider.BadEvents.goodLocalEventAt_triadicCubeShift {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : Frozen.Section3.goodLocalEventAt M Ccg Q.scale n (HCPolySupport.triadicCubeShift Q) = goodLocalEvent M Ccg Q n

Pulling the centred good local event back by the positive base-point translation gives the cube-indexed good local event exactly.