OAI/Probability/GaussianReplacement/ConditionalInfo.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.conditionalMutualInformation line 15

    Also declared: ComparatorChallenges/GaussianReplacement.lean:96 (same declaration text).

  2. lemma OAI.CurrentProjection.kernel_prod_eq_compProd line 24
  3. lemma OAI.CurrentProjection.compProd_prod_assoc line 31
  4. def OAI.CurrentProjection.swapAssoc line 38
  5. lemma OAI.CurrentProjection.compProd_prod_swapAssoc line 42
  6. lemma OAI.CurrentProjection.fst_map_swapAssoc_compProd line 51
  7. lemma OAI.CurrentProjection.conditionalKL_chain line 61
  8. def OAI.CurrentProjection.mutualInformation line 80
  9. lemma OAI.CurrentProjection.fst_map_assoc_compProd line 83
  10. lemma OAI.CurrentProjection.mutualInformation_chain line 90
  11. lemma OAI.CurrentProjection.conditionalMutualInformation_le_entropy line 130
  12. lemma OAI.CurrentProjection.conditionalMutualInformation_compProd line 146
  13. lemma OAI.CurrentProjection.conditionalMutualInformation_map_right_le line 157
  14. lemma OAI.CurrentProjection.rowInformation_eq_conditionalMutualInformation line 199
  15. lemma OAI.CurrentProjection.conditionalMutualInformation_swap line 232
  16. lemma OAI.CurrentProjection.rowInformation_eq_sourceConditionalInformation line 265
  17. def OAI.CurrentProjection.actualConditionalRowInformation line 290

    Also declared: ComparatorChallenges/GaussianReplacement.lean:181 (same declaration text).

  18. structure OAI.CurrentProjection.ActualRowSourceConclusion line 295

    Also declared: ComparatorChallenges/GaussianReplacement.lean:186 (same declaration text).

  19. theorem OAI.CurrentProjection.actualRowSourceMain line 329

    Distinct definitions of this name: ComparatorChallenges/GaussianReplacement.lean:468 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.actualRowSourceMain@path.

  20. theorem OAI.CurrentProjection.actualRowSourceRefinement line 365

    Distinct definitions of this name: ComparatorChallenges/GaussianReplacement.lean:489 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.actualRowSourceRefinement@path.

  21. def OAI.CurrentProjection.alignedExperiment line 400

    Also declared: ComparatorChallenges/GaussianReplacement.lean:220 (same declaration text).

  22. lemma OAI.CurrentProjection.measurable_alignedMap line 404
  23. instance OAI.CurrentProjection.alignedExperiment_probability line 408

    Also declared: ComparatorChallenges/GaussianReplacement.lean:224 (same declaration text).

  24. def OAI.CurrentProjection.exposedJointMap line 414

    Also declared: ComparatorChallenges/GaussianReplacement.lean:230 (same declaration text).

  25. lemma OAI.CurrentProjection.measurable_exposedJointMap line 417
  26. def OAI.CurrentProjection.exposedInformation line 423

    Also declared: ComparatorChallenges/GaussianReplacement.lean:233 (same declaration text).