OAI/Analysis/VlasovMaxwell/Model.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The one-species relativistic Vlasov–Maxwell system on three-dimensional Euclidean space.

  1. abbrev OAI.RVM.Vec line 13

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:10 (same declaration text).

  2. abbrev OAI.RVM.Phase line 14

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:11 (same declaration text).

  3. abbrev OAI.RVM.Particle line 15

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:12 (same declaration text).

  4. abbrev OAI.RVM.Field line 16

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:13 (same declaration text).

  5. def OAI.RVM.q line 18

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:15 (same declaration text).

  6. def OAI.RVM.velocity line 19

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:16 (same declaration text).

  7. def OAI.RVM.basis line 21

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:18 (same declaration text).

  8. def OAI.RVM.dot line 22

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:19 (same declaration text).

  9. def OAI.RVM.cross line 23

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:20 (same declaration text).

  10. def OAI.RVM.spatialPartial line 27

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:24 (same declaration text).

  11. def OAI.RVM.divergence line 29

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:26 (same declaration text).

  12. def OAI.RVM.curl line 32

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:29 (same declaration text).

  13. def OAI.RVM.rho line 37

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:34 (same declaration text).

  14. def OAI.RVM.current line 38

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:35 (same declaration text).

  15. structure OAI.RVM.Datum line 41

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:38 (same declaration text).

  16. def OAI.RVM.BoundedSmooth line 46

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:43 (same declaration text).

  17. def OAI.RVM.Admissible line 50

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:47 (same declaration text).

  18. structure OAI.RVM.Solution line 57

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:54 (same declaration text).

  19. def OAI.RVM.particleHalfSpace line 62

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:59 (same declaration text).

  20. def OAI.RVM.fieldHalfSpace line 63

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:60 (same declaration text).

  21. def OAI.RVM.particleSlab line 64

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:61 (same declaration text).

  22. def OAI.RVM.fieldSlab line 65

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:62 (same declaration text).

  23. def OAI.RVM.TimeContinuousL2 line 67

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:64 (same declaration text).

  24. def OAI.RVM.Equations line 72

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:69 (same declaration text).

  25. def OAI.RVM.CompactOnFiniteHorizons line 85

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:82 (same declaration text).

  26. def OAI.RVM.Classical line 89

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:86 (same declaration text).

  27. def OAI.RVM.SmoothOnFiniteHorizons line 98

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:95 (same declaration text).

  28. def OAI.RVM.SameNonnegativeTime line 102

    Also declared: ComparatorChallenges/VlasovMaxwell.lean:99 (same declaration text).