OAI/Probability/FreeIsing/Trees/InfiniteCanonicalPathResponse.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.CavityFieldLimit.finiteSiteField_eq_treeField line 22
  2. def OAI.Problem367.CavityFieldLimit.rootResponseProduct line 29
  3. theorem OAI.Problem367.CavityFieldLimit.infiniteCavityField_eq_snd line 36
  4. theorem OAI.Problem367.CavityFieldLimit.measurable_rootResponseProduct line 44
  5. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_rootResponse_eq_canonical_product line 57
  6. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsRootResponse_eq_canonical_product line 117
  7. theorem OAI.Problem367.HasFreeIsingLaw.infiniteGibbsRootResponse_brownian_eq_canonical_product line 130
  8. theorem OAI.Problem367.HasFreeIsingLaw.brownian_past_rootResponse_eq_canonical_product line 151