OAI/Analysis/VlasovMaxwell/Flow/TransportDifferentiation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.sphere_mean_zero_lipschitz_bound line 19
  2. def OAI.RVM.transportSingularShell line 43
  3. lemma OAI.RVM.transport_divergence_sphere_continuous line 47
  4. lemma OAI.RVM.transportSingularShell_near_far line 58
  5. lemma OAI.RVM.transportSingularShell_continuousOn line 103
  6. lemma OAI.RVM.physical_transport_log_bound line 152
  7. lemma OAI.RVM.singular_radial_log_bound_norm line 180
  8. lemma OAI.RVM.integral_annulus_polar_radial line 193
  9. def OAI.RVM.transportSingularBulk line 229
  10. lemma OAI.RVM.transportSingularBulk_continuousOn line 232
  11. lemma OAI.RVM.transportSingularBulk_shell line 268
  12. lemma OAI.RVM.transportSingularBulk_annulus line 315
  13. lemma OAI.RVM.physical_transport_annulus_log_bound line 325
  14. lemma OAI.RVM.transportSpatialFlux_uniform_bound line 358
  15. lemma OAI.RVM.transport_sphere_rescale line 373
  16. lemma OAI.RVM.transport_sphere_boundary_bound line 391
  17. def OAI.RVM.transportVelocityProfile line 424
  18. lemma OAI.RVM.transportVelocityProfile_contDiffAt line 429
  19. lemma OAI.RVM.divergence_parameter_slice line 445
  20. lemma OAI.RVM.continuousOn_transportVelocityDivergence line 457
  21. lemma OAI.RVM.transportVelocityDivergence_uniform_bound line 471
  22. lemma OAI.RVM.divergence_real_const_smul line 490
  23. lemma OAI.RVM.transport_velocity_divergence_rescale line 499
  24. lemma OAI.RVM.physical_transport_velocity_bound line 518
  25. lemma OAI.RVM.norm_integral_annulus_inverse_sq_le line 533
  26. def OAI.RVM.transportVelocityBulk line 561
  27. lemma OAI.RVM.transport_velocity_annulus_bound line 566
  28. lemma OAI.RVM.transport_velocity_divergence_continuousOn line 605
  29. lemma OAI.RVM.shifted_particle_continuousOn line 619
  30. lemma OAI.RVM.transport_bulk_split line 628
  31. lemma OAI.RVM.transport_sphere_support line 696
  32. lemma OAI.RVM.abs_sub_sub_add_le line 711
  33. lemma OAI.RVM.electric_transport_annulus_gradient_bound line 715
  34. lemma OAI.RVM.integral_symmetric_annulus_tendsto line 760
  35. lemma OAI.RVM.norm_integral_ball_of_annulus_bound line 786
  36. lemma OAI.RVM.particle_spatial_fderiv line 794
  37. lemma OAI.RVM.transportConeCoefficient_uniform_bound line 803
  38. lemma OAI.RVM.transport_derivative_integrable line 826
  39. lemma OAI.RVM.electric_transport_gradient_bound line 882
  40. lemma OAI.RVM.particle_fixed_time_contDiff line 909
  41. lemma OAI.RVM.transport_kernel_velocity_contDiff line 915
  42. lemma OAI.RVM.hasDerivAt_transport_particle_line line 921
  43. lemma OAI.RVM.norm_transport_velocity_integral_le line 959
  44. lemma OAI.RVM.transport_density_integrable line 981
  45. lemma OAI.RVM.hasDerivAt_electric_transport_integral line 1012
  46. lemma OAI.RVM.electric_transport_deriv_bound line 1059