OAI/Analysis/SymmetricDomains/WeightedTaylorUniformlyCompact.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Release061.analytic_normal_offset_noncollapseline 36 - def
OAI.Release061.parabolicScaleline 68 - lemma
OAI.Release061.parabolicScale_normline 70 - lemma
OAI.Release061.parabolic_cubic_remainderline 80 - lemma
OAI.Release061.multilinear_one_evalline 112 - lemma
OAI.Release061.parabolic_partialSumline 117 - theorem
OAI.Release061.parabolic_taylor_uniformly_compactline 141 - lemma
OAI.Release061.uniform_reindexline 173 - def
OAI.Release061.weightedScaleline 178 - lemma
OAI.Release061.sqrt_tendsto_posline 181 - theorem
OAI.Release061.weighted_taylor_uniformly_compactline 190