OAI/Analysis/AncientFlat/Evolution/TraceFour.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalIBP.D line 13
  2. lemma OAI.ClassicalIBP.contDiff_D line 16
  3. lemma OAI.ClassicalIBP.D_D_eq line 21
  4. lemma OAI.ClassicalIBP.integral_D_right line 28
  5. lemma OAI.ClassicalIBP.integral_D_D_right line 43
  6. lemma OAI.ClassicalIBP.laplacian_eq_sum_D line 51
  7. lemma OAI.ClassicalIBP.integral_laplacian_right line 60
  8. lemma OAI.ClassicalIBP.contDiff_laplacian line 75
  9. lemma OAI.ClassicalIBP.compactSupport_laplacian line 86
  10. lemma OAI.ClassicalIBP.integral_bilaplacian_right line 103
  11. def OAI.ClassicalIBP.directional line 116
  12. lemma OAI.ClassicalIBP.iteratedFDeriv_eq_directional line 121
  13. lemma OAI.ClassicalIBP.D_sum line 137
  14. lemma OAI.ClassicalIBP.laplacian_sum line 145
  15. def OAI.ClassicalIBP.traceFour line 154
  16. lemma OAI.ClassicalIBP.bilaplacian_eq_traceFour line 160