OAI/Probability/InvariantIsing/Fields/FieldTerminalOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The final covariance coordinate has the same mixed monotonicity; its backward derivative has the additional constant one half.

  1. def OAI.InvariantIsing.fieldTerminalFamily line 15
  2. lemma OAI.InvariantIsing.fieldTerminalFamily_value_eq_operator line 20
  3. lemma OAI.InvariantIsing.fieldTerminalFamily_mean_eq_transition line 27
  4. theorem OAI.InvariantIsing.fieldTerminalFamily_tangent line 38
  5. theorem OAI.InvariantIsing.fieldTerminalFamily_tangent_antitone line 59
  6. theorem OAI.InvariantIsing.fieldTerminalFamily_shape line 78
  7. theorem OAI.InvariantIsing.fieldTerminal_earlier_squares_antitone line 111