OAI/Geometry/TamingCompatibility/DifferentialForms/GreenNeg.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HilbertSobolev.greenNegOne line 14
  2. lemma OAI.TamingCompatibility.HilbertSobolev.greenNegOne_distribution line 16
  3. lemma OAI.TamingCompatibility.HilbertSobolev.helmholtz_greenNegOne line 22
  4. def OAI.TamingCompatibility.HilbertSobolev.weakValue line 28
  5. def OAI.TamingCompatibility.HilbertSobolev.weakGradient line 32
  6. lemma OAI.TamingCompatibility.HilbertSobolev.weakValue_distribution line 36
  7. lemma OAI.TamingCompatibility.HilbertSobolev.weakGradient_distribution line 40
  8. lemma OAI.TamingCompatibility.HilbertSobolev.weakValue_norm_le line 47
  9. lemma OAI.TamingCompatibility.HilbertSobolev.weakGradient_norm_le line 51
  10. lemma OAI.TamingCompatibility.HilbertSobolev.product_zero_distribution line 57
  11. lemma OAI.TamingCompatibility.HilbertSobolev.derivative_zero_distribution line 61
  12. def OAI.TamingCompatibility.HilbertSobolev.negativeProductMain line 65
  13. def OAI.TamingCompatibility.HilbertSobolev.negativeProductTerm line 69
  14. lemma OAI.TamingCompatibility.HilbertSobolev.negativeProductMain_distribution line 74
  15. lemma OAI.TamingCompatibility.HilbertSobolev.negativeProductTerm_distribution line 80
  16. def OAI.TamingCompatibility.HilbertSobolev.productNegOne line 89
  17. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_productNegOne line 93
  18. lemma OAI.TamingCompatibility.HilbertSobolev.product_zero_le_size_one line 103
  19. lemma OAI.TamingCompatibility.HilbertSobolev.negativeProductMain_norm_le line 108
  20. lemma OAI.TamingCompatibility.HilbertSobolev.negativeProductTerm_norm_le line 116
  21. lemma OAI.TamingCompatibility.HilbertSobolev.productNegOne_norm_le line 140
  22. lemma OAI.TamingCompatibility.HilbertSobolev.productNegOne_operator_estimate line 156