OAI/Analysis/Triangular/Schwartz/GaussianPair.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.AtomicTriangular.gaussianSchwartzline 12 - lemma
OAI.AtomicTriangular.gaussianSchwartz_applyline 14 - lemma
OAI.AtomicTriangular.gaussianSchwartz_coeline 17 - lemma
OAI.AtomicTriangular.gaussian_radialline 19 - lemma
OAI.AtomicTriangular.realFourier_gaussianline 22 - lemma
OAI.AtomicTriangular.realFourier_smulline 34 - lemma
OAI.AtomicTriangular.realFourier_subline 41 - structure
OAI.AtomicTriangular.GaussianPairline 49 - def
OAI.AtomicTriangular.largeGaussianPairline 61 - def
OAI.AtomicTriangular.reciprocalGaussianPairline 73 - def
OAI.AtomicTriangular.gaussianPairline 111 - theorem
OAI.AtomicTriangular.sharp_gaussian_minorantsline 115