OAI/Analysis/TriangularHilbert/Model.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TriangularHilbert.Plane line 12

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

2. structure OAI.TriangularHilbert.Endpoints line 14

   Also declared: ComparatorChallenges/TriangularHilbert.lean:14 (same declaration text).

3. def OAI.TriangularHilbert.annulus line 20

   Also declared: ComparatorChallenges/TriangularHilbert.lean:20 (same declaration text).

4. def OAI.TriangularHilbert.integrand line 22

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

5. def OAI.TriangularHilbert.truncation line 25

   Also declared: ComparatorChallenges/TriangularHilbert.lean:25 (same declaration text).

6. def OAI.TriangularHilbert.GoodPoint line 28

   Also declared: ComparatorChallenges/TriangularHilbert.lean:28 (same declaration text).

7. def OAI.TriangularHilbert.maximal line 32

   Also declared: ComparatorChallenges/TriangularHilbert.lean:32 (same declaration text).

8. def OAI.TriangularHilbert.maximalNorm line 37

   Also declared: ComparatorChallenges/TriangularHilbert.lean:37 (same declaration text).

9. def OAI.TriangularHilbert.MainEstimate line 40

   Distinct definitions of this name: ComparatorChallenges/TriangularHilbert.lean:40 (same statement text; different proof or body). Qualify references as OAI.TriangularHilbert.MainEstimate@path.