OAI/Probability/SKFluctuations/CavityGraphParity.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Cavity Graph Parity.

  1. def OAI.SKFluctuations.Cavity.siteMonomial line 21
  2. def OAI.SKFluctuations.Cavity.blockDegree line 27
  3. theorem OAI.SKFluctuations.Cavity.siteMonomial_gauge line 32
  4. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_graph_odd line 49
  5. theorem OAI.SKFluctuations.Cavity.blockDegree_append line 65
  6. theorem OAI.SKFluctuations.Cavity.blockDegree_pair_even line 74
  7. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_zero_low line 91
  8. theorem OAI.SKFluctuations.Cavity.cutSitePair_frozen_decomposition line 109
  9. def OAI.SKFluctuations.Hierarchy.ClockExpr.iterSource line 140
  10. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.iterSource_append line 145
  11. theorem OAI.SKFluctuations.Hierarchy.ClockTree.eval_iterSource_testExpr line 152
  12. theorem OAI.SKFluctuations.Hierarchy.ClockTree.eval_iterSource_abs_le line 177
  13. def OAI.SKFluctuations.Hierarchy.ReplicaTree.splitIndex line 199
  14. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.splitIndex_symm line 207
  15. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.splitIndex_le line 214
  16. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.splitIndex_self line 221
  17. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_preserves_split line 228
  18. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_variation line 251
  19. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_leaves line 258
  20. def OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairExpectation line 268
  21. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairExpectation_const line 277
  22. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairExpectation_add line 282
  23. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairExpectation_smul line 289
  24. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.marked_list_weight_abs_le line 297
  25. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePairExpectation_abs_le line 312
  26. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.profileTerm line 353
  27. def OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRowList line 359
  28. def OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow line 364
  29. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profilePair_eq_rows line 369
  30. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_const_separable line 377
  31. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_add line 386
  32. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_smul line 393
  33. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileTerm_fresh_zero line 400
  34. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileTerm_left line 407
  35. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileTerm_right line 424
  36. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileTerm_cross_left_zero line 432
  37. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileTerm_cross_right_zero line 439
  38. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRowList_map_left line 446
  39. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRowList_map_right line 460
  40. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRowList_smooth line 483
  41. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileTerm_step line 493
  42. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRowList_map_step line 509
  43. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_step_zero line 530
  44. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_fork_left_zero line 545
  45. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.profileRow_fork_right_zero line 566