OAI/Probability/InvariantIsing/Cavity/CavityFiniteDeficitPath.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The finite overlap quantile, held constant beyond its last level, and the strictly decreasing deficits on its active cascade steps.

  1. def OAI.InvariantIsing.cavityFiniteLevel line 14
  2. lemma OAI.InvariantIsing.cavityFiniteLevel_zero line 17
  3. lemma OAI.InvariantIsing.cavityFiniteLevel_last line 21
  4. lemma OAI.InvariantIsing.cavityFiniteLevel_castSucc line 25
  5. lemma OAI.InvariantIsing.cavityFiniteLevel_succ line 30
  6. lemma OAI.InvariantIsing.cavityFiniteLevel_monotone line 35
  7. def OAI.InvariantIsing.cavityFiniteDeficitPath line 39
  8. lemma OAI.InvariantIsing.cavityFiniteDeficitPath_antitone line 42
  9. lemma OAI.InvariantIsing.cavityFiniteDeficitPath_pos line 46
  10. lemma OAI.InvariantIsing.cavityFiniteDeficitPath_step line 53
  11. lemma OAI.InvariantIsing.cavityFiniteDeficitPath_step_strict line 69
  12. lemma OAI.InvariantIsing.finite_chainExponent_pos line 84
  13. lemma OAI.InvariantIsing.field_chainExponent_pos line 92