OAI/Analysis/TriangularHilbert/HardPairing.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TriangularHilbert.Heat.hardKernelline 11 - lemma
OAI.TriangularHilbert.Heat.hardKernel_decompositionline 14 - lemma
OAI.TriangularHilbert.Heat.selectedSum_le_no_finsetline 26 - def
OAI.TriangularHilbert.Heat.hardPairingConstantline 50 - lemma
OAI.TriangularHilbert.Heat.hardPairingConstant_posline 51 - lemma
OAI.TriangularHilbert.Heat.hardPairing_leline 55