OAI/Probability/InvariantIsing/Fields/FieldEndpointMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The canonical terminal field has a depth-independent second moment, controlled by the initial bias and the final covariance height.

  1. lemma OAI.InvariantIsing.fieldTailVariance_total line 16
  2. theorem OAI.InvariantIsing.fieldCanonicalEndpointLaw_mgf line 28
  3. lemma OAI.InvariantIsing.sq_le_exp_two_add line 60
  4. theorem OAI.InvariantIsing.fieldCanonicalEndpointLaw_second_moment line 72