OAI/Geometry/TamingCompatibility/DifferentialForms/Product.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.HilbertSobolev.product line 14
2. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_product line 18
3. lemma OAI.TamingCompatibility.HilbertSobolev.product_inclusion line 22
4. lemma OAI.TamingCompatibility.HilbertSobolev.product_derivative line 29
5. lemma OAI.TamingCompatibility.HilbertSobolev.product_zero_eq line 48
6. lemma OAI.TamingCompatibility.HilbertSobolev.product_zero_norm_le line 60
7. def OAI.TamingCompatibility.HilbertSobolev.coefficientSize line 68
8. lemma OAI.TamingCompatibility.HilbertSobolev.coefficientSize_nonneg line 74
9. lemma OAI.TamingCompatibility.HilbertSobolev.coefficientSize_le_succ line 80
10. lemma OAI.TamingCompatibility.HilbertSobolev.coefficientSize_derivative_le line 85
11. theorem OAI.TamingCompatibility.HilbertSobolev.product_estimate line 92
12. theorem OAI.TamingCompatibility.HilbertSobolev.product_operator_estimate line 157