OAI/Probability/InvariantIsing/Cavity/CavityOneReplicaPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

One sampled innovation path has independent Gaussian increments. This is the marginal needed by the remaining linear-tilt moment bound.

  1. lemma OAI.InvariantIsing.cavity_replica_one_marginal line 14
  2. lemma OAI.InvariantIsing.cavity_edgeAt_injective line 23
  3. lemma OAI.InvariantIsing.cavity_selected_path_law line 29
  4. lemma OAI.InvariantIsing.cavity_coordinate_one_path_law line 41
  5. theorem OAI.InvariantIsing.cavity_marked_one_path_law line 63
  6. lemma OAI.InvariantIsing.cavityLeafSum_eq_mark_sum line 73