OAI/Analysis/StrictMeans/Model.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StrictInverseFirstPower.disk line 11

   Also declared: ComparatorChallenges/StrictMeans.lean:10 (same declaration text).

2. def OAI.StrictInverseFirstPower.NormalizedUnivalent line 13

   Also declared: ComparatorChallenges/StrictMeans.lean:12 (same declaration text).

3. def OAI.StrictInverseFirstPower.BoundedNormalizedUnivalent line 16

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

4. def OAI.StrictInverseFirstPower.integralMean line 19

   Also declared: ComparatorChallenges/StrictMeans.lean:18 (same declaration text).

5. def OAI.StrictInverseFirstPower.growthExponent line 23

   Also declared: ComparatorChallenges/StrictMeans.lean:22 (same declaration text).

6. def OAI.StrictInverseFirstPower.boundedSpectrum line 28

   Also declared: ComparatorChallenges/StrictMeans.lean:27 (same declaration text).

7. def OAI.StrictInverseFirstPower.kraetzerPrediction line 31

   Also declared: ComparatorChallenges/StrictMeans.lean:30 (same declaration text).