OAI/Analysis/TriangularHilbert/Main.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularHilbert.maximal_eq_cyclicMax_ae line 11
2. lemma OAI.TriangularHilbert.aemeasurable_maximal line 19
3. lemma OAI.TriangularHilbert.maximalNorm_eq_cyclicNorm line 25
4. theorem OAI.TriangularHilbert.main_estimate line 38

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