OAI/Analysis/TriangularHilbert/GroupedGaussian.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TriangularHilbert.Heat.groupWeightline 16 - def
OAI.TriangularHilbert.Heat.groupFirstline 19 - def
OAI.TriangularHilbert.Heat.groupSecondline 22 - lemma
OAI.TriangularHilbert.Heat.groupWeight_posline 27 - lemma
OAI.TriangularHilbert.Heat.groupWeight_hasDerivAt_centerline 32 - lemma
OAI.TriangularHilbert.Heat.groupFirst_hasDerivAt_centerline 43 - lemma
OAI.TriangularHilbert.Heat.groupFirst_hasDerivAt_otherline 53 - lemma
OAI.TriangularHilbert.Heat.groupWeight_hasDerivAt_varianceline 60 - lemma
OAI.TriangularHilbert.Heat.groupEnergy_hasDerivAt_centerline 70 - lemma
OAI.TriangularHilbert.Heat.groupEnergyFirst_hasDerivAt_centerline 80 - lemma
OAI.TriangularHilbert.Heat.groupEnergyFirst_hasDerivAt_otherline 97 - lemma
OAI.TriangularHilbert.Heat.groupEnergy_hasDerivAt_varianceline 113