OAI/Analysis/TriangularHilbert/CubicApprox.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.TriangularHilbert.lintegral_enorm_cubeline 13 - lemma
OAI.TriangularHilbert.norm_cube_le_four_subline 19 - lemma
OAI.TriangularHilbert.tendsto_of_enorm_cubeline 29 - lemma
OAI.TriangularHilbert.exists_cubic_approximationline 41