OAI/Analysis/AffineBernstein/FlatLogCalculus.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.AffineBernstein.dirDeriv_const_mulline 15 - lemma
OAI.AffineBernstein.dirDeriv_expMulline 19 - lemma
OAI.AffineBernstein.second_dirDeriv_const_mulline 24 - lemma
OAI.AffineBernstein.second_dirDeriv_expMulline 34 - lemma
OAI.AffineBernstein.second_dirDeriv_congrline 53