OAI/Probability/InvariantIsing/Cavity/CavityStrictUniformPath.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite overlap paths with strictly increasing interior levels. Their endpoint convention is fixed, and they converge to the original quantile almost everywhere and in L1.

  1. def OAI.InvariantIsing.cavityUniformLevel line 16
  2. lemma OAI.InvariantIsing.cavityUniformLevel_monotone line 19
  3. lemma OAI.InvariantIsing.cavityUniformLevel_on_cell line 25
  4. lemma OAI.InvariantIsing.cavity_uniform_epsilon line 32
  5. def OAI.InvariantIsing.cavityStrictUniformLevels line 38
  6. lemma OAI.InvariantIsing.cavityStrictUniformLevels_mem line 41
  7. lemma OAI.InvariantIsing.cavityStrictUniformLevels_strict line 47
  8. def OAI.InvariantIsing.cavityStrictUniformPath line 54
  9. lemma OAI.InvariantIsing.cavityStrictUniformPath_on_cell line 60
  10. lemma OAI.InvariantIsing.cavityStrictUniformPath_dist line 66
  11. lemma OAI.InvariantIsing.cavityStrictUniformPath_ae_tendsto line 73
  12. lemma OAI.InvariantIsing.cavityStrictUniformPath_l1_tendsto line 84