OAI/Probability/InvariantIsing/Gaussian/GaussianExponentialShift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Completing the square under the finite scalar Gaussian law. This is the shift identity used to control canonical increments uniformly in the number and size of the cascade steps.

  1. lemma OAI.InvariantIsing.gaussianPDFReal_exp_linear line 15
  2. theorem OAI.InvariantIsing.gaussian_exp_linear_shift line 27