OAI/Probability/InvariantIsing/Fields/FieldAdjacentOrder.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual internal-height comparison in fld:mixed. The fixed tail is the finite log-cosh recursion. Increasing one height adds its parameter to one variance and subtracts it from the next variance.

  1. def OAI.InvariantIsing.fieldAdjacentTail line 17
  2. def OAI.InvariantIsing.fieldAdjacentInner line 24
  3. def OAI.InvariantIsing.fieldAdjacentFamily line 31
  4. lemma OAI.InvariantIsing.fieldAdjacentTail_stationary line 38
  5. lemma OAI.InvariantIsing.fieldAdjacentInner_shape line 43
  6. lemma OAI.InvariantIsing.fieldAdjacentFamily_shape line 67
  7. theorem OAI.InvariantIsing.fieldAdjacentFamily_tangent_antitone line 97
  8. theorem OAI.InvariantIsing.fieldAdjacent_earlier_squares_antitone line 120