OAI/Probability/FreeIsing/Gaussian/BinaryFusionJointLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.binaryFusionJointLaw line 11
  2. theorem OAI.Problem367.integral_id_eq_zero_of_neg_invariant line 14
  3. theorem OAI.Problem367.integrable_id_of_ae_abs_lt_one line 22
  4. theorem OAI.Problem367.binaryFusionJointLaw_probability line 29
  5. theorem OAI.Problem367.integral_binaryFusion_sq_jointLaw line 51
  6. theorem OAI.Problem367.binaryFusionJointLaw_secondMoment line 64
  7. theorem OAI.Problem367.binaryFusionJointLaw_secondMoment_le line 74
  8. theorem OAI.Problem367.binaryFusionJointLaw_neg_invariant line 86
  9. theorem OAI.Problem367.binaryFusion_map_neg_invariant line 103
  10. theorem OAI.Problem367.binaryFusion_map_abs_lt_one line 128
  11. theorem OAI.Problem367.binaryFusion_map_probability line 143