OAI/Probability/StrongRayleigh/Main.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336AdditiveD139.finite_strongly_rayleigh_response line 21

    Distinct definitions of this name: ComparatorChallenges/StronglyRayleighDPP.lean:132 (same statement text; different proof or body). Qualify references as OAI.Problem336AdditiveD139.finite_strongly_rayleigh_response@path.

  2. theorem OAI.Problem336AdditiveD139.strongly_rayleigh_group_factor line 39

    Distinct definitions of this name: ComparatorChallenges/StronglyRayleighDPP.lean:147 (same statement text; different proof or body). Qualify references as OAI.Problem336AdditiveD139.strongly_rayleigh_group_factor@path.

  3. theorem OAI.Problem336AdditiveD139.finite_positive_contraction_dpp_is_strongly_rayleigh line 48

    Distinct definitions of this name: ComparatorChallenges/StronglyRayleighDPP.lean:153 (same statement text; different proof or body). Qualify references as OAI.Problem336AdditiveD139.finite_positive_contraction_dpp_is_strongly_rayleigh@path.

  4. theorem OAI.Problem336AdditiveD139.countable_positive_contraction_dpp_exists_unique line 57

    Distinct definitions of this name: ComparatorChallenges/StronglyRayleighDPP.lean:161 (same statement text; different proof or body). Qualify references as OAI.Problem336AdditiveD139.countable_positive_contraction_dpp_exists_unique@path.

  5. theorem OAI.Problem336AdditiveD139.invariant_positive_contraction_dpp_factor line 65

    Distinct definitions of this name: ComparatorChallenges/StronglyRayleighDPP.lean:167 (same statement text; different proof or body). Qualify references as OAI.Problem336AdditiveD139.invariant_positive_contraction_dpp_factor@path.

  6. theorem OAI.Problem336AdditiveD139.translation_invariant_kernel_dpp_factor line 75

    Distinct definitions of this name: ComparatorChallenges/StronglyRayleighDPP.lean:174 (same statement text; different proof or body). Qualify references as OAI.Problem336AdditiveD139.translation_invariant_kernel_dpp_factor@path.