OAI/Analysis/CoulombIonization/FormDomain/L2.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoulombSobolev.L2 line 25
  2. structure OAI.CoulombSobolev.Test line 27
  3. def OAI.CoulombSobolev.Test.deriv line 34
  4. lemma OAI.CoulombSobolev.Test.memLp line 40
  5. def OAI.CoulombSobolev.Test.toL2 line 44
  6. lemma OAI.CoulombSobolev.Test.coe_toL2 line 47
  7. lemma OAI.CoulombSobolev.Test.inner_toL2 line 51
  8. lemma OAI.CoulombSobolev.test_total line 61
  9. def OAI.CoulombSobolev.Test.tensor line 96
  10. lemma OAI.CoulombSobolev.Test.tensor_toL2 line 105
  11. lemma OAI.CoulombSobolev.Test.tensor_deriv line 119
  12. def OAI.CoulombSobolev.HasWeakPartialDerivative line 139
  13. lemma OAI.CoulombSobolev.partial_derivative_adjoint_zero line 143
  14. lemma OAI.CoulombSobolev.projected_test_derivative line 153
  15. lemma OAI.CoulombSobolev.projected_weak_derivative line 169