OAI/Probability/GaussianReplacement/Comparison.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentProjection.criticalFamily_projection_ac line 13
2. lemma OAI.CurrentProjection.criticalFamily_actual_log_bound line 26
3. lemma OAI.CurrentProjection.critical_refined_comparison line 62
4. lemma OAI.CurrentProjection.critical_unrefined_comparison line 106
5. lemma OAI.CurrentProjection.critical_entropy_scalars line 156
6. lemma OAI.CurrentProjection.critical_dimensions line 179
7. lemma OAI.CurrentProjection.uniformSphere_probability_of_pos line 185

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

8. theorem OAI.CurrentProjection.criticalComparisonMain line 197

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

9. def OAI.CurrentProjection.OneLevelComparisonMain line 233

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

10. def OAI.CurrentProjection.TwoLabelComparisonMain line 243

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

11. lemma OAI.CurrentProjection.level_entropy_scalars line 252
12. lemma OAI.CurrentProjection.oneLevel_dimensions line 271
13. lemma OAI.CurrentProjection.twoLabel_dimensions line 277
14. theorem OAI.CurrentProjection.oneLevelComparisonMain line 286

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

15. theorem OAI.CurrentProjection.twoLabelComparisonMain line 325

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