OAI/Analysis/VlasovMaxwell/Retarded/RetardedPhaseDomain.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.retardedPhaseDomain line 31
  2. def OAI.RVM.initialConeLabels line 34
  3. lemma OAI.RVM.isOpen_retardedPhaseDomain line 36
  4. lemma OAI.RVM.retarded_emission_mem line 40
  5. lemma OAI.RVM.PhaseFlowOn.retarded_injective line 44
  6. lemma OAI.RVM.PhaseFlowOn.exists_emission line 63
  7. lemma OAI.RVM.PhaseFlowOn.retarded_image line 77
  8. def OAI.RVM.VlasovOn line 123
  9. lemma OAI.RVM.PhaseFlowOn.transport line 130
  10. lemma OAI.RVM.PhaseFlowOn.transport_inverse line 155
  11. lemma OAI.RVM.PhaseFlowOn.transport_nonneg line 162
  12. lemma OAI.RVM.PhaseFlowOn.transport_integral line 169
  13. lemma OAI.RVM.PhaseFlowOn.retarded_integral line 199
  14. def OAI.RVM.PhaseFlowOn.retardedSource line 229
  15. lemma OAI.RVM.PhaseFlowOn.retardedSource_label line 234
  16. lemma OAI.RVM.PhaseFlowOn.retarded_integral_inverse line 251
  17. lemma OAI.RVM.PhaseFlowOn.retarded_transport_integral line 265
  18. structure OAI.RVM.EnergyPrefix line 282
  19. lemma OAI.RVM.EnergyPrefix.differentiable_particle line 300
  20. lemma OAI.RVM.EnergyPrefix.differentiable_field line 304
  21. lemma OAI.RVM.EnergyPrefix.local_data line 308
  22. lemma OAI.RVM.EnergyPrefix.spacetime_vlasov line 322
  23. lemma OAI.RVM.EnergyPrefix.particle_energy_balance line 329
  24. lemma OAI.RVM.EnergyPrefix.particle_energy_flux_regular line 338
  25. lemma OAI.RVM.EnergyPrefix.particleFlux_component line 352
  26. lemma OAI.RVM.EnergyPrefix.particle_energy_local line 358
  27. lemma OAI.RVM.EnergyPrefix.local_energy_conservation line 378
  28. lemma OAI.RVM.EnergyPrefix.velocity_slice line 413
  29. lemma OAI.RVM.EnergyPrefix.particle_energy_nonneg line 426
  30. lemma OAI.RVM.EnergyPrefix.particle_flux_bound line 432
  31. lemma OAI.RVM.EnergyPrefix.total_energy_nonneg line 448
  32. lemma OAI.RVM.EnergyPrefix.total_flux_bound line 454
  33. lemma OAI.RVM.EnergyPrefix.prefix_memLp line 460
  34. lemma OAI.RVM.EnergyPrefix.prefix_integrable_norm_sq line 466
  35. lemma OAI.RVM.EnergyPrefix.prefix_continuous_integral_norm_sq line 472
  36. lemma OAI.RVM.EnergyPrefix.particle_energy_continuous_slab line 484
  37. lemma OAI.RVM.EnergyPrefix.particle_energy_compact line 499
  38. lemma OAI.RVM.EnergyPrefix.particle_energy_integrable line 511
  39. lemma OAI.RVM.EnergyPrefix.total_energy_integrable line 519
  40. lemma OAI.RVM.EnergyPrefix.integrated_energy_continuous line 525
  41. lemma OAI.RVM.EnergyPrefix.total_energy_regular line 548
  42. lemma OAI.RVM.EnergyPrefix.total_flux_regular line 556
  43. lemma OAI.RVM.EnergyPrefix.deriv_weighted_energy line 565
  44. lemma OAI.RVM.EnergyPrefix.total_energy_continuous_slab line 608
  45. lemma OAI.RVM.EnergyPrefix.weighted_energy_continuous line 614
  46. lemma OAI.RVM.EnergyPrefix.weighted_energy_deriv_bound line 623
  47. lemma OAI.RVM.EnergyPrefix.weighted_energy_increment_bound line 648
  48. theorem OAI.RVM.EnergyPrefix.energy_conservation line 665
  49. lemma OAI.RVM.Classical.energyPrefix line 689