OAI/Probability/InvariantIsing/Fields/FieldAffineRecursion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite scalar log-cosh recursion with affine covariance increments is a smooth field family on its strict covariance interval.

  1. def OAI.InvariantIsing.fieldLogCoshFamily line 14
  2. structure OAI.InvariantIsing.FieldAffineStep line 49
  3. def OAI.InvariantIsing.fieldAffineValue line 54
  4. def OAI.InvariantIsing.fieldAffineFamily line 59
  5. theorem OAI.InvariantIsing.fieldAffineFamily_value line 67
  6. theorem OAI.InvariantIsing.fieldAffineValue_hasFDerivAt line 78