OAI/Analysis/IntegralMeans/Model.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Brennan.disk line 10

   Also declared: ComparatorChallenges/Brennan.lean:10 (same declaration text), ComparatorChallenges/BrennanSharp.lean:10 (same declaration text).

2. def OAI.Brennan.UnivalentOn line 12

   Also declared: ComparatorChallenges/Brennan.lean:12 (same declaration text), ComparatorChallenges/BrennanSharp.lean:12 (same declaration text).

3. def OAI.Brennan.Schlicht line 15

   Also declared: ComparatorChallenges/Brennan.lean:15 (same declaration text), ComparatorChallenges/BrennanSharp.lean:15 (same declaration text).

4. def OAI.Brennan.integralMean line 18

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

5. def OAI.Brennan.beta line 22

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

6. def OAI.Brennan.spectrum line 27

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

7. def OAI.Brennan.SphericalBoundaryNontrivial line 30

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

8. def OAI.Brennan.MainStatement line 33

   Also declared: ComparatorChallenges/Brennan.lean:33 (same declaration text).