OAI/Analysis/VlasovMaxwell/Regularity/EnergyBump.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.deriv_time_slice line 15
  2. lemma OAI.RVM.spatialPartial_time_slice line 21
  3. lemma OAI.RVM.classical_particleFlux_component line 27
  4. lemma OAI.RVM.classical_particle_energy_local line 34
  5. lemma OAI.RVM.field_differentiableAt_positive line 55
  6. lemma OAI.RVM.divergence_add line 65
  7. lemma OAI.RVM.classical_local_energy_conservation line 78
  8. lemma OAI.RVM.classical_velocity_slice line 117
  9. lemma OAI.RVM.classical_particle_energy_nonneg line 131
  10. lemma OAI.RVM.classical_particle_flux_bound line 138
  11. lemma OAI.RVM.classical_total_energy_nonneg line 155
  12. lemma OAI.RVM.classical_total_flux_bound line 162
  13. lemma OAI.RVM.continuousOn_integral_uniform_support line 169
  14. lemma OAI.RVM.TimeContinuousL2.memLp line 186
  15. lemma OAI.RVM.TimeContinuousL2.integrable_norm_sq line 191
  16. lemma OAI.RVM.TimeContinuousL2.continuous_integral_norm_sq line 196
  17. lemma OAI.RVM.classical_particle_energy_continuous_slab line 207
  18. lemma OAI.RVM.classical_particle_energy_compact line 223
  19. lemma OAI.RVM.classical_particle_energy_integrable line 236
  20. lemma OAI.RVM.classical_total_energy_integrable line 245
  21. lemma OAI.RVM.classical_integrated_energy_continuous line 252
  22. lemma OAI.RVM.classical_total_energy_regular line 276
  23. lemma OAI.RVM.classical_total_flux_regular line 287
  24. lemma OAI.RVM.integral_mul_divergence line 299
  25. lemma OAI.RVM.deriv_weighted_energy line 321
  26. lemma OAI.RVM.classical_total_energy_continuous_slab line 365
  27. lemma OAI.RVM.classical_weighted_energy_continuous line 373
  28. lemma OAI.RVM.weighted_energy_deriv_bound line 383
  29. lemma OAI.RVM.weighted_energy_increment_bound line 409
  30. def OAI.RVM.energyBump line 427
  31. def OAI.RVM.energyCutoff line 428
  32. lemma OAI.RVM.energyCutoff_smooth line 430
  33. lemma OAI.RVM.energyCutoff_compact line 434
  34. lemma OAI.RVM.energyCutoff_bounds line 449
  35. lemma OAI.RVM.energyCutoff_deriv_bound line 452
  36. lemma OAI.RVM.energyCutoff_tendsto line 474
  37. lemma OAI.RVM.energyCutoff_integral_tendsto line 480
  38. theorem OAI.RVM.classical_energy_conservation line 493
  39. lemma OAI.RVM.scalar_gronwall_interior line 529
  40. lemma OAI.RVM.weighted_density_hasDerivAt line 557
  41. lemma OAI.RVM.continuous_divergence line 588
  42. lemma OAI.RVM.weighted_density_deriv_le line 597
  43. theorem OAI.RVM.local_energy_inequality_vanishes line 647
  44. def OAI.RVM.RegularParticle line 699
  45. lemma OAI.RVM.Classical.regularParticle line 703
  46. lemma OAI.RVM.RegularParticle.local_data line 706
  47. lemma OAI.RVM.RegularParticle.slice line 714
  48. def OAI.RVM.particleMoment line 727
  49. lemma OAI.RVM.RegularParticle.moment_integrable line 731
  50. lemma OAI.RVM.RegularParticle.moment_regular line 738
  51. lemma OAI.RVM.RegularParticle.moment_continuous_slab line 751
  52. lemma OAI.RVM.RegularParticle.moment_compact line 769
  53. lemma OAI.RVM.RegularParticle.spatial_moment_integrable line 782
  54. lemma OAI.RVM.RegularParticle.integrated_moment_continuous line 792
  55. lemma OAI.RVM.RegularParticle.velocity_flux_bound line 800
  56. lemma OAI.RVM.TimeContinuousL2.sub line 817
  57. lemma OAI.RVM.uniqueDiffOn_particleHalfSpace line 826
  58. lemma OAI.RVM.RegularParticle.velocity_derivative_bound line 832
  59. lemma OAI.RVM.integral_lorentz_derivative_zero line 871
  60. lemma OAI.RVM.particle_number_balance_param line 878
  61. lemma OAI.RVM.fderiv_square_half line 944
  62. def OAI.RVM.squareDifference line 954
  63. lemma OAI.RVM.squareDifference_nonneg line 957
  64. lemma OAI.RVM.squareDifference_zero_iff line 960
  65. lemma OAI.RVM.particle_difference_direction line 964