OAI/Analysis/TriangularHilbert/IntMax.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularHilbert.mem_intInterval_iff_dist line 10
2. def OAI.TriangularHilbert.supportRadius line 19
3. def OAI.TriangularHilbert.intAverage line 21
4. lemma OAI.TriangularHilbert.intAverage_nonneg line 24
5. lemma OAI.TriangularHilbert.inter_intInterval_of_supportRadius_le line 28
6. def OAI.TriangularHilbert.intMax line 35
7. lemma OAI.TriangularHilbert.intAverage_le_intMax line 38
8. lemma OAI.TriangularHilbert.intMax_nonneg line 51
9. lemma OAI.TriangularHilbert.intMax_attained line 54
10. lemma OAI.TriangularHilbert.sum_interval_le_intMax line 60