OAI/Analysis/TriangularHilbert/DiscretePairing.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TriangularHilbert.Heat.kernelOutputline 14 - def
OAI.TriangularHilbert.Heat.kernelPairingline 17 - lemma
OAI.TriangularHilbert.Heat.kernelPairing_eqline 20 - lemma
OAI.TriangularHilbert.Heat.kernelPairing_addline 32 - lemma
OAI.TriangularHilbert.Heat.kernelPairing_const_mulline 36 - lemma
OAI.TriangularHilbert.Heat.kernelPairing_smoothline 47