OAI/Probability/InvariantIsing/Gaussian/GaussianTiltIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The canonical one-step Gaussian increment satisfies the sharp exponential bound from the magnetic replacement argument. Its cost is proportional to variance, so it can be summed over arbitrary depths.

  1. theorem OAI.InvariantIsing.gaussian_tilt_increment_mgf line 15