OAI/Probability/InvariantIsing/Gaussian/GaussianGramTransformLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the actual positive Gram transforms at every positive real argument.

  1. lemma OAI.InvariantIsing.gaussianGramTransform_error_bound_tendsto line 12
  2. theorem OAI.InvariantIsing.gaussianGramTransform_mean_tendsto line 29
  3. theorem OAI.InvariantIsing.gaussianPatternStieltjes_L1 line 37