OAI/Probability/FreeIsing/Ising/OrientedPrefixWeights.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.IsingOrientedPath.takeVertex_takeVertex_of_le line 17
  2. theorem OAI.Problem367.IsingOrientedPath.edge_takeVertex line 22
  3. theorem OAI.Problem367.IsingOrientedPath.logSum_prefix line 28
  4. def OAI.Problem367.IsingOrientedPath.extensionAt line 38
  5. theorem OAI.Problem367.IsingOrientedPath.endpoint_extensionAt line 42
  6. theorem OAI.Problem367.IsingOrientedPath.prefix_edges_in_stem line 47
  7. theorem OAI.Problem367.IsingOrientedPath.exists_logSum_prefix_variance_bound line 57
  8. theorem OAI.Problem367.IsingOrientedPath.integral_prefix_weight_mul_le_of_tail line 95