OAI/Probability/StrongRayleigh/Model.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem336AdditiveD139.UnitLabel line 15

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:15 (same declaration text).

2. def OAI.Problem336AdditiveD139.leftTranslate line 17

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:17 (same declaration text).

3. def OAI.Problem336AdditiveD139.iidUnitLabels line 20

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:20 (same declaration text).

4. def OAI.Problem336AdditiveD139.InvariantBinaryLaw line 23

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:23 (same declaration text).

5. def OAI.Problem336AdditiveD139.HasEquivariantIIDFactor line 29

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:29 (same declaration text).

6. def OAI.Problem336AdditiveD139.finiteGeneratingValue line 37

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:37 (same declaration text).

7. def OAI.Problem336AdditiveD139.StronglyRayleighFinite line 44

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:44 (same declaration text).

8. def OAI.Problem336AdditiveD139.marginalMass line 48

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:48 (same declaration text).

9. def OAI.Problem336AdditiveD139.marginalGeneratingValue line 52

   Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:52 (same declaration text).

10. def OAI.Problem336AdditiveD139.StronglyRayleighCountable line 59

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:59 (same declaration text).

11. def OAI.Problem336AdditiveD139.boolReal line 64

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:64 (same declaration text).

12. def OAI.Problem336AdditiveD139.tiltPartition line 66

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:66 (same declaration text).

13. def OAI.Problem336AdditiveD139.tiltMean line 73

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:73 (same declaration text).

14. def OAI.Problem336AdditiveD139.tiltSecondMoment line 81

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:81 (same declaration text).

15. def OAI.Problem336AdditiveD139.tiltCovariance line 90

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:90 (same declaration text).

16. def OAI.Problem336AdditiveD139.coordinatePerturb line 94

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:94 (same declaration text).

17. def OAI.Problem336AdditiveD139.PositiveContractionFinite line 98

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:98 (same declaration text).

18. def OAI.Problem336AdditiveD139.IsFiniteDeterminantalLaw line 106

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:106 (same declaration text).

19. def OAI.Problem336AdditiveD139.PositiveContractionKernel line 113

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:113 (same declaration text).

20. def OAI.Problem336AdditiveD139.IsDeterminantalLaw line 121

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:121 (same declaration text).

21. def OAI.Problem336AdditiveD139.TranslationInvariantKernel line 128

    Also declared: ComparatorChallenges/StronglyRayleighDPP.lean:128 (same declaration text).