OAI/Probability/FreeIsing/Estimates/KernelCompatibility.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.KernelCompatibility.map_compProd_comap line 14
  2. theorem OAI.Problem367.KernelCompatibility.map_compProd_of_kernel_map_ae line 25
  3. theorem OAI.Problem367.KernelCompatibility.map_reorder_compProd line 43
  4. theorem OAI.Problem367.KernelCompatibility.map_reorder_compProd_of_ae line 62
  5. theorem OAI.Problem367.KernelCompatibility.indepFun_future_of_past_kernel line 74
  6. theorem OAI.Problem367.KernelCompatibility.map_reorder_conditionalCopies line 95
  7. theorem OAI.Problem367.KernelCompatibility.indepFun_future_conditionalCopies line 117
  8. theorem OAI.Problem367.KernelCompatibility.map_conditionalCopies_of_jointLaw line 145
  9. theorem OAI.Problem367.KernelCompatibility.indepFun_of_joint_product line 174
  10. theorem OAI.Problem367.KernelCompatibility.indepFun_future_conditionalCopies_of_jointLaw line 193
  11. def OAI.Problem367.KernelCompatibility.reorderEquiv line 211
  12. theorem OAI.Problem367.KernelCompatibility.exists_past_kernel_of_indep line 223
  13. theorem OAI.Problem367.KernelCompatibility.indepFun_future_conditionalCopies_of_original_indep line 271
  14. theorem OAI.Problem367.KernelCompatibility.exists_past_kernel_of_indep_of_embedding line 286
  15. theorem OAI.Problem367.KernelCompatibility.indepFun_future_conditionalCopies_of_embedding line 356
  16. theorem OAI.Problem367.KernelCompatibility.indepFun_future_conditionalCopies_of_reconstructible_split line 377