OAI/Probability/InvariantIsing/Arrays/ReplicaWardPaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Extract pointwise path equations from continuous Ward tests, then pass those equations to symbols and right roots. All Ward hypotheses in this module are internal consequences to be supplied by rotation calculus.

  1. def OAI.InvariantIsing.offWardPath line 19
  2. def OAI.InvariantIsing.diagonalWardResidual line 22
  3. lemma OAI.InvariantIsing.ae_offWardPath_zero_of_tests line 25
  4. lemma OAI.InvariantIsing.intervalIntegrable_replicaProductPath line 72
  5. lemma OAI.InvariantIsing.pathSymbol_ward_linear line 101
  6. lemma OAI.InvariantIsing.pathSymbol_zero_of_ae line 113
  7. theorem OAI.InvariantIsing.offWardPath_symbol line 127
  8. theorem OAI.InvariantIsing.offWardPath_root line 148