OAI/Geometry/TamingCompatibility/DifferentialForms/UniformScaledJet.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TamingCompatibility.HilbertSobolev.uniform_scaled_two_jet line 21
2. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_Hsucc_norm_le line 94
3. lemma OAI.TamingCompatibility.HilbertSobolev.schwartz_L2_support_bound line 108
4. theorem OAI.TamingCompatibility.HilbertSobolev.schwartz_Hnat_support_bound line 123
5. lemma OAI.TamingCompatibility.HilbertSobolev.rescaleSchwartz_iterated line 155