OAI/Probability/FreeIsing/Trees/CanonicalPathResponse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.FinitePathGibbs.mean_eq_posterior_mean line 13
  2. theorem OAI.Problem367.FinitePathGibbs.coordinate_mean_mem_Ioo line 26
  3. theorem OAI.Problem367.FinitePathGibbs.coordinate_mean_affine line 37
  4. theorem OAI.Problem367.FinitePathGibbs.backwardField_eq_cavityFromSites line 53
  5. theorem OAI.Problem367.TreePathResponse.measurable_mean line 70
  6. theorem OAI.Problem367.TreePathResponse.measurable_field line 76

    Distinct definitions of this name: OAI/Probability/FreeIsing/Trees/ResponseFieldBound.lean:10 (different declaration text). Qualify references as OAI.Problem367.TreePathResponse.measurable_field@path.

  7. def OAI.Problem367.TreePathResponse.orientedCavity line 84
  8. theorem OAI.Problem367.TreePathResponse.measurable_orientedCavity line 90
  9. theorem OAI.Problem367.TreePathResponse.root_response_eq_canonical_product line 97