OAI/Analysis/VlasovMaxwell/Maxwell/DifferenceFieldEnergy.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.difference_source_pointwise line 17
  2. lemma OAI.RVM.compact_difference_source_bound line 47
  3. lemma OAI.RVM.squareDifference_regular line 90
  4. lemma OAI.RVM.particleMoment_one line 108
  5. lemma OAI.RVM.RegularParticle.moment_component line 112
  6. lemma OAI.RVM.particle_difference_local line 119
  7. lemma OAI.RVM.curl_sub line 155
  8. lemma OAI.RVM.difference_maxwell_local line 166
  9. def OAI.RVM.differenceFieldEnergy line 205
  10. def OAI.RVM.differenceEnergy line 208
  11. def OAI.RVM.differenceFlux line 211
  12. lemma OAI.RVM.differenceFieldEnergy_nonneg line 214
  13. lemma OAI.RVM.differenceEnergy_nonneg line 218
  14. lemma OAI.RVM.differenceEnergy_regular line 224
  15. lemma OAI.RVM.differenceFlux_regular line 234
  16. lemma OAI.RVM.differenceEnergy_continuous_slab line 245
  17. lemma OAI.RVM.differenceEnergy_integrable line 255
  18. lemma OAI.RVM.differenceEnergy_integrated_continuous line 262
  19. lemma OAI.RVM.differenceFlux_bound line 285
  20. lemma OAI.RVM.differenceEnergy_initial line 295
  21. lemma OAI.RVM.differenceEnergy_local line 304
  22. lemma OAI.RVM.differenceEnergy_zero line 381
  23. lemma OAI.RVM.differenceEnergy_differential_bound line 411
  24. theorem OAI.RVM.classical_unique line 441
  25. lemma OAI.RVM.vacuum_energy_conservation line 464
  26. lemma OAI.RVM.vacuum_memLp line 487
  27. lemma OAI.RVM.norm_sub_sq_le_twice line 512
  28. lemma OAI.RVM.pair_sq_difference_tendsto line 517
  29. lemma OAI.RVM.L2_norm_sub_sq_eq_integral line 587
  30. lemma OAI.RVM.timeContinuousL2_of_continuous_energy line 597
  31. theorem OAI.RVM.vacuum_timeContinuousL2 line 639
  32. def OAI.RVM.freeMaxwellElectric line 657
  33. def OAI.RVM.freeMaxwellMagnetic line 660
  34. lemma OAI.RVM.initialCharge_conserved line 662
  35. lemma OAI.RVM.freeMaxwell_equations line 671
  36. theorem OAI.RVM.freeMaxwell_evolution line 687
  37. lemma OAI.RVM.derivWithin_slice_eq_dirD line 715
  38. theorem OAI.RVM.global_classical_solution_of_zero_particles line 723