OAI/Analysis/VlasovMaxwell/Geometry/SpaceDiv.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.spaceDiv line 12
  2. lemma OAI.RVM.contDiff_spaceDiv line 15
  3. lemma OAI.RVM.spaceDiv_slice line 19
  4. lemma OAI.RVM.dirD_spaceDiv line 29
  5. lemma OAI.RVM.spaceDiv_spaceCurl line 39
  6. lemma OAI.RVM.dirD_component_fun line 47
  7. lemma OAI.RVM.waveBox_dirD_zero line 52
  8. lemma OAI.RVM.waveBox_spaceCurl_zero line 63
  9. def OAI.RVM.freeField line 78
  10. lemma OAI.RVM.freeField_apply line 81
  11. lemma OAI.RVM.contDiff_freeField line 84
  12. lemma OAI.RVM.freeField_initial line 91
  13. lemma OAI.RVM.freeField_initial_deriv line 96
  14. lemma OAI.RVM.freeField_box line 104
  15. lemma OAI.RVM.field_wave_initial_second line 117
  16. def OAI.RVM.vacuumElectric line 127
  17. def OAI.RVM.vacuumMagnetic line 128
  18. lemma OAI.RVM.contDiff_vacuumElectric line 130
  19. lemma OAI.RVM.contDiff_vacuumMagnetic line 135
  20. lemma OAI.RVM.spaceCurl_of_slice_eq line 140
  21. lemma OAI.RVM.dirD_neg_field line 146
  22. lemma OAI.RVM.wave_maxwell_residual line 150
  23. lemma OAI.RVM.vacuumElectric_initial line 189
  24. lemma OAI.RVM.vacuumMagnetic_initial line 193
  25. lemma OAI.RVM.vacuum_maxwell_first_order line 197
  26. def OAI.RVM.fieldBox line 245
  27. lemma OAI.RVM.fieldBox_apply line 248
  28. lemma OAI.RVM.contDiff_fieldBox line 251
  29. lemma OAI.RVM.fieldBox_add line 257
  30. lemma OAI.RVM.fieldBox_sub line 263
  31. lemma OAI.RVM.fieldBox_neg line 269
  32. lemma OAI.RVM.fieldBox_dirD line 274
  33. lemma OAI.RVM.fieldBox_spaceCurl line 282
  34. lemma OAI.RVM.waveGradient_add line 296
  35. lemma OAI.RVM.waveGradient_sub line 302
  36. lemma OAI.RVM.waveGradient_neg line 308
  37. lemma OAI.RVM.dirD_waveGradient line 313
  38. lemma OAI.RVM.spaceCurl_waveGradient line 319
  39. lemma OAI.RVM.fieldBox_waveGradient line 328
  40. lemma OAI.RVM.fieldBox_curl_curl line 333
  41. lemma OAI.RVM.waveGradient_eq_of_eventuallyEq line 346
  42. lemma OAI.RVM.field_wave_zero line 351
  43. def OAI.RVM.electricResidual line 366
  44. def OAI.RVM.magneticResidual line 369
  45. lemma OAI.RVM.contDiff_electricResidual line 372
  46. lemma OAI.RVM.contDiff_magneticResidual line 377
  47. lemma OAI.RVM.electricResidual_box line 381
  48. lemma OAI.RVM.magneticResidual_box line 411
  49. lemma OAI.RVM.electricResidual_initial_deriv line 431