OAI/Probability/FreeIsing/Conditioning/DiscreteConditioning.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.condExp_comap_eq_cond_on_fiber line 15
  2. theorem OAI.Problem367.condExp_indicator_comap_eq_cond_on_fiber line 55
  3. theorem OAI.Problem367.indepFun_cond_fiber_of_condIndepFun line 62
  4. theorem OAI.Problem367.iIndepFun_cond_fiber_of_iCondIndepFun line 90
  5. theorem OAI.Problem367.condExp_comap_discrete line 125
  6. theorem OAI.Problem367.condIndepFun_iff_indepFun_cond_fibers line 139
  7. theorem OAI.Problem367.ae_of_ae_restrict_fibers line 179
  8. theorem OAI.Problem367.iCondIndepFun_iff_iIndepFun_cond_fibers line 189