OAI/Probability/InvariantIsing/Gaussian/GaussianTiltLinearGrowth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Linear-growth observables are integrable under finite Gaussian tilts with linear-growth potentials. This supplies the actual recursive loss integrals, without extra moment hypotheses.

  1. lemma OAI.InvariantIsing.exponentialNormMoments_tilted line 14
  2. lemma OAI.InvariantIsing.integrable_linearGrowth_tilted line 37