OAI/Probability/StrongRayleigh/PairCoefficients.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.tiltPairMass line 14
  2. lemma OAI.Problem336AdditiveD139.tiltPairMass_nonneg line 22
  3. lemma OAI.Problem336AdditiveD139.tiltPartition_pairMass line 33
  4. lemma OAI.Problem336AdditiveD139.tiltMean_pairMass_left line 45
  5. lemma OAI.Problem336AdditiveD139.tiltMean_pairMass_right line 58
  6. lemma OAI.Problem336AdditiveD139.tiltSecondMoment_pairMass line 71
  7. lemma OAI.Problem336AdditiveD139.tiltCovariance_pairMass line 82
  8. lemma OAI.Problem336AdditiveD139.tiltCovariance_nonpos_of_pairMass line 96
  9. def OAI.Problem336AdditiveD139.pairSlice line 104
  10. lemma OAI.Problem336AdditiveD139.prod_pairSlice line 108
  11. lemma OAI.Problem336AdditiveD139.tiltPairMass_generating line 119