OAI/Probability/ThorpResults/SignedBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.signedEntropy line 11

   Also declared: ComparatorChallenges/ThorpRemaining.lean:452 (same declaration text).

2. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.budgetCoefficient line 15

   Also declared: ComparatorChallenges/ThorpRemaining.lean:456 (same declaration text).

3. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.remainderBudget line 18

   Also declared: ComparatorChallenges/ThorpRemaining.lean:459 (same declaration text).

4. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.logWeightedMoment line 23

   Distinct definitions of this name: ComparatorChallenges/ThorpRemaining.lean:464 (same statement text; different proof or body). Qualify references as OAI.ThorpNine.Harmonic.Thorp.LowPlanes.logWeightedMoment@path.

5. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.row_entropy_nonneg line 26
6. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.signedEntropy_nonneg line 36
7. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.budgetCoefficient_nonneg line 41
8. lemma OAI.ThorpNine.Harmonic.Thorp.LowPlanes.remainderBudget_nonneg line 49
9. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.signed_occurrence_moment line 55