OAI/Geometry/TamingCompatibility/DifferentialForms/FiberMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HilbertSobolev.fiberMap line 17
  2. lemma OAI.TamingCompatibility.HilbertSobolev.fiberMap_apply line 22
  3. lemma OAI.TamingCompatibility.HilbertSobolev.fiberMap_bessel line 26
  4. lemma OAI.TamingCompatibility.HilbertSobolev.fiberMap_derivative line 33
  5. lemma OAI.TamingCompatibility.HilbertSobolev.fiberMap_product line 40
  6. lemma OAI.TamingCompatibility.HilbertSobolev.fiberMap_Lp line 45
  7. lemma OAI.TamingCompatibility.HilbertSobolev.MemSobolev_fiberMap line 56
  8. def OAI.TamingCompatibility.HilbertSobolev.fiberOperator line 62
  9. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_fiberOperator line 65
  10. def OAI.TamingCompatibility.HilbertSobolev.matrixLowerOrder line 77
  11. lemma OAI.TamingCompatibility.HilbertSobolev.matrixLowerOrder_memSobolev line 83
  12. theorem OAI.TamingCompatibility.HilbertSobolev.matrix_cutoff_H1_regular line 100