OAI/Probability/InvariantIsing/Magnetic/RestrictedFieldTerminal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual constrained-block terminal payoff. Its prior mass is not renormalized; the Lipschitz and growth estimates include that fixed mass.

  1. lemma OAI.InvariantIsing.restrictedSpinLog_le_add line 16
  2. lemma OAI.InvariantIsing.abs_restrictedSpinLog_sub_le line 22
  3. def OAI.InvariantIsing.restrictedFieldTerminal line 33
  4. lemma OAI.InvariantIsing.restrictedFieldTerminal_univ line 36
  5. lemma OAI.InvariantIsing.restrictedFieldTerminal_zero line 40
  6. lemma OAI.InvariantIsing.restrictedFieldTerminal_le_univ line 44
  7. lemma OAI.InvariantIsing.restrictedFieldTerminal_difference line 49
  8. lemma OAI.InvariantIsing.restrictedFieldTerminal_norm_difference line 54
  9. lemma OAI.InvariantIsing.continuous_restrictedFieldTerminal line 63
  10. lemma OAI.InvariantIsing.restrictedFieldTerminal_linearGrowth line 71
  11. lemma OAI.InvariantIsing.restrictedFieldTerminal_group_bias line 81