OAI/Probability/InvariantIsing/Fields/FieldHeightCone.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The strict finite field-height cone and its original FieldStep representatives. Positive increments give every height and order constraint.

  1. def OAI.InvariantIsing.fieldStrictHeightCone line 14
  2. lemma OAI.InvariantIsing.continuous_fieldHeightIncrement line 17
  3. lemma OAI.InvariantIsing.isOpen_fieldStrictHeightCone line 22
  4. lemma OAI.InvariantIsing.fieldHeightIncrement_succ line 27
  5. lemma OAI.InvariantIsing.fieldStrictHeightCone_strictMono line 34
  6. lemma OAI.InvariantIsing.fieldStrictHeightCone_nonneg line 42
  7. lemma OAI.InvariantIsing.convex_fieldStrictHeightCone line 47
  8. def OAI.InvariantIsing.fieldStepOfStrictHeights line 62
  9. lemma OAI.InvariantIsing.fieldStepOfStrictHeights_strict line 66
  10. lemma OAI.InvariantIsing.fieldHeightJointValue_strict line 70