OAI/Geometry/TamingCompatibility/DifferentialForms/PerturbationNeg.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.HilbertSobolev.perturbationNegOne line 15
  2. lemma OAI.TamingCompatibility.HilbertSobolev.toDistribution_perturbationNegOne line 21
  3. lemma OAI.TamingCompatibility.HilbertSobolev.perturbedHelmholtz_negOne_toDistribution line 37
  4. def OAI.TamingCompatibility.HilbertSobolev.weakPrincipalCoefficientSize line 48
  5. lemma OAI.TamingCompatibility.HilbertSobolev.weakPrincipalCoefficientSize_nonneg line 53
  6. lemma OAI.TamingCompatibility.HilbertSobolev.perturbationNegOne_norm_le line 59
  7. theorem OAI.TamingCompatibility.HilbertSobolev.perturbedHelmholtz_solve_negOne line 78
  8. theorem OAI.TamingCompatibility.HilbertSobolev.weak_H1_regular line 100
  9. theorem OAI.TamingCompatibility.HilbertSobolev.weak_succ_regular line 116
  10. lemma OAI.TamingCompatibility.HilbertSobolev.coefficient_products_commute line 138
  11. def OAI.TamingCompatibility.HilbertSobolev.secondCommutator line 145
  12. lemma OAI.TamingCompatibility.HilbertSobolev.distribution_second_product line 151
  13. lemma OAI.TamingCompatibility.HilbertSobolev.secondCommutator_memSobolev line 159
  14. def OAI.TamingCompatibility.HilbertSobolev.localizationError line 171
  15. lemma OAI.TamingCompatibility.HilbertSobolev.helmholtz_cutoff line 179
  16. lemma OAI.TamingCompatibility.HilbertSobolev.perturbedHelmholtz_cutoff line 191
  17. lemma OAI.TamingCompatibility.HilbertSobolev.localizationError_memSobolev line 200
  18. theorem OAI.TamingCompatibility.HilbertSobolev.cutoff_H1_regular line 209
  19. def OAI.TamingCompatibility.HilbertSobolev.lowerOrder line 224
  20. lemma OAI.TamingCompatibility.HilbertSobolev.lowerOrder_memSobolev line 228
  21. theorem OAI.TamingCompatibility.HilbertSobolev.full_operator_H1_regular line 238