OAI/Analysis/VlasovMaxwell/Retarded/SourceField.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.magneticResidual_initial_deriv line 11
  2. lemma OAI.RVM.wave_system_implies_maxwell line 33
  3. def OAI.RVM.sourceField line 67
  4. lemma OAI.RVM.sourceField_apply line 70
  5. lemma OAI.RVM.contDiff_sourceField line 73
  6. lemma OAI.RVM.sourceField_initial line 79
  7. lemma OAI.RVM.sourceField_initial_deriv line 83
  8. lemma OAI.RVM.sourceField_box line 89
  9. lemma OAI.RVM.freeField_fieldBox line 94
  10. def OAI.RVM.maxwellElectric line 99
  11. def OAI.RVM.maxwellMagnetic line 103
  12. lemma OAI.RVM.contDiff_maxwellElectric line 106
  13. lemma OAI.RVM.contDiff_maxwellMagnetic line 113
  14. lemma OAI.RVM.maxwellElectric_initial line 119
  15. lemma OAI.RVM.maxwellMagnetic_initial line 123
  16. lemma OAI.RVM.maxwellElectric_initial_deriv line 127
  17. lemma OAI.RVM.maxwellMagnetic_initial_deriv line 140
  18. lemma OAI.RVM.maxwellElectric_box line 151
  19. lemma OAI.RVM.maxwellMagnetic_box line 162
  20. lemma OAI.RVM.spaceDiv_of_slice_eq line 172
  21. lemma OAI.RVM.maxwell_first_order line 178
  22. lemma OAI.RVM.spaceDiv_add line 205
  23. lemma OAI.RVM.spaceDiv_sub line 210
  24. lemma OAI.RVM.spaceDiv_neg line 215
  25. lemma OAI.RVM.scalar_time_constant line 219
  26. lemma OAI.RVM.maxwell_gauss_propagation line 237
  27. theorem OAI.RVM.constructed_maxwell_equations line 270
  28. lemma OAI.RVM.causal_local_energy_bound line 293
  29. lemma OAI.RVM.coneCutoff_one_on_ball line 334
  30. lemma OAI.RVM.causal_energy_integrable line 342
  31. lemma OAI.RVM.divergence_neg line 385
  32. lemma OAI.RVM.causal_energy_conserved line 390
  33. def OAI.RVM.maxwellEnergy line 422
  34. def OAI.RVM.maxwellFlux line 424
  35. lemma OAI.RVM.contDiff_maxwellEnergy line 426
  36. lemma OAI.RVM.contDiff_maxwellFlux line 429
  37. lemma OAI.RVM.maxwellEnergy_nonneg line 432
  38. lemma OAI.RVM.maxwellFlux_le line 435