OAI/Probability/InvariantIsing/Fields/FieldVaryingRecursion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fixed finite cascade exponents with varying nonnegative scalar variances. These are the actual log-cosh recursion and spin observables.

  1. def OAI.InvariantIsing.fieldVaryingValue line 16
  2. def OAI.InvariantIsing.fieldVaryingMean line 19
  3. def OAI.InvariantIsing.fieldVaryingSquares line 24
  4. lemma OAI.InvariantIsing.fieldVaryingValue_eq_scalar line 31
  5. lemma OAI.InvariantIsing.fieldVaryingMean_eq_scalar line 36
  6. lemma OAI.InvariantIsing.fieldVaryingSquares_eq_scalar line 45
  7. lemma OAI.InvariantIsing.fieldVaryingValue_regular line 65
  8. lemma OAI.InvariantIsing.fieldVaryingMean_regular line 74
  9. lemma OAI.InvariantIsing.fieldVaryingSquares_regular line 85
  10. lemma OAI.InvariantIsing.fieldVaryingValue_nonneg line 97
  11. def OAI.InvariantIsing.fieldVaryingCap line 114
  12. lemma OAI.InvariantIsing.fieldVaryingValue_bound line 117