OAI/Analysis/VlasovMaxwell/Maxwell/WaveGradient.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.dirD_component line 32
  2. lemma OAI.RVM.divergence_smul line 41
  3. def OAI.RVM.waveGradient line 58
  4. lemma OAI.RVM.waveGradient_apply line 61
  5. lemma OAI.RVM.contDiff_waveGradient line 64
  6. lemma OAI.RVM.waveGradient_slice line 70
  7. lemma OAI.RVM.divergence_waveGradient line 76
  8. lemma OAI.RVM.waveGradient_time line 83
  9. def OAI.RVM.waveEnergy line 90
  10. def OAI.RVM.waveFlux line 93
  11. lemma OAI.RVM.contDiff_waveEnergy line 96
  12. lemma OAI.RVM.contDiff_waveFlux line 100
  13. lemma OAI.RVM.waveEnergy_nonneg line 103
  14. lemma OAI.RVM.waveFlux_bound line 107
  15. lemma OAI.RVM.waveEnergy_deriv line 114
  16. lemma OAI.RVM.waveFlux_divergence line 133
  17. lemma OAI.RVM.wave_local_energy line 163
  18. lemma OAI.RVM.dirD_add line 169
  19. lemma OAI.RVM.dirD_sub line 176
  20. lemma OAI.RVM.dirD_sum line 183
  21. lemma OAI.RVM.dirD_third_comm line 190
  22. def OAI.RVM.waveBox line 199
  23. lemma OAI.RVM.waveBox_eq line 203
  24. lemma OAI.RVM.contDiff_waveBox line 208
  25. lemma OAI.RVM.waveBox_sub line 212
  26. lemma OAI.RVM.waveBox_add line 224
  27. lemma OAI.RVM.waveBox_dirD line 236
  28. lemma OAI.RVM.waveBox_timeDerivative_zero line 249
  29. lemma OAI.RVM.waveK_box line 258
  30. def OAI.RVM.freeWave line 262
  31. lemma OAI.RVM.contDiff_freeWave line 265
  32. lemma OAI.RVM.freeWave_initial line 269
  33. lemma OAI.RVM.freeWave_initial_velocity line 274
  34. lemma OAI.RVM.freeWave_box line 287
  35. lemma OAI.RVM.sourceWave_box line 295
  36. lemma OAI.RVM.waveGradient_initial_zero line 300
  37. lemma OAI.RVM.waveEnergy_initial_zero line 308
  38. lemma OAI.RVM.wave_zero_on line 315
  39. lemma OAI.RVM.wave_zero line 348
  40. lemma OAI.RVM.wave_unique line 354
  41. lemma OAI.RVM.wave_unique_on line 373
  42. def OAI.RVM.retardedWave line 393
  43. lemma OAI.RVM.contDiff_retardedWave line 396
  44. lemma OAI.RVM.retardedWave_initial line 401
  45. lemma OAI.RVM.retardedWave_initial_velocity line 405
  46. lemma OAI.RVM.retardedWave_box line 418
  47. lemma OAI.RVM.wave_representation line 426
  48. lemma OAI.RVM.wave_representation_on line 436
  49. def OAI.RVM.curlA line 447
  50. def OAI.RVM.curlB line 448
  51. def OAI.RVM.spaceCurl line 450
  52. lemma OAI.RVM.spaceCurl_apply line 454
  53. lemma OAI.RVM.contDiff_spaceCurl line 458
  54. lemma OAI.RVM.spaceCurl_slice line 464
  55. lemma OAI.RVM.dirD_spaceCurl line 475
  56. lemma OAI.RVM.spaceCurl_sub line 489
  57. lemma OAI.RVM.spaceCurl_add line 496
  58. lemma OAI.RVM.spaceCurl_neg line 503
  59. lemma OAI.RVM.contDiff_field_slice line 509
  60. lemma OAI.RVM.spaceCurl_spaceCurl_component line 512
  61. lemma OAI.RVM.dirD_eq_of_eventuallyEq line 521
  62. lemma OAI.RVM.positive_time_eventuallyEq line 527
  63. lemma OAI.RVM.spaceCurl_eq_of_eventuallyEq line 533
  64. lemma OAI.RVM.interval_time_eventuallyEq line 538
  65. lemma OAI.RVM.dirD_dirD_component line 544
  66. lemma OAI.RVM.waveBox_component_eq line 551
  67. lemma OAI.RVM.maxwell_electric_wave line 557
  68. lemma OAI.RVM.maxwell_magnetic_wave line 579
  69. lemma OAI.RVM.dirD_spatial_slice line 627
  70. lemma OAI.RVM.waveBox_dirD_sourceWave line 632
  71. lemma OAI.RVM.sourceWave_space_initial line 639
  72. lemma OAI.RVM.sourceWave_time_initial line 647
  73. lemma OAI.RVM.sourceWave_time_time_initial line 652
  74. lemma OAI.RVM.sourceWave_space_time_initial line 661
  75. def OAI.RVM.electricPotentialComponent line 671
  76. lemma OAI.RVM.contDiff_electricPotentialComponent line 674
  77. lemma OAI.RVM.electricPotentialComponent_initial line 680
  78. lemma OAI.RVM.electricPotentialComponent_initial_velocity line 686
  79. lemma OAI.RVM.waveBox_neg line 700
  80. lemma OAI.RVM.electricPotentialComponent_box line 710
  81. lemma OAI.RVM.maxwell_electric_potential_representation line 723
  82. def OAI.RVM.magneticPotentialComponent line 758
  83. lemma OAI.RVM.contDiff_magneticPotentialComponent line 762
  84. lemma OAI.RVM.magneticPotentialComponent_initial line 767
  85. lemma OAI.RVM.magneticPotentialComponent_initial_velocity line 771
  86. lemma OAI.RVM.magneticPotentialComponent_box line 781
  87. lemma OAI.RVM.maxwell_magnetic_potential_representation line 793