OAI/Analysis/VlasovMaxwell/Retarded/TransportAngularCore.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.Magnetic.transportAngularCore line 15
  2. def OAI.RVM.Magnetic.sourceAngularCore line 18
  3. lemma OAI.RVM.Magnetic.physicalMagneticKernel_eulerian_split line 21
  4. lemma OAI.RVM.Magnetic.coneRadius_zero_smul line 28
  5. lemma OAI.RVM.Magnetic.coneDirection_zero_smul line 32
  6. lemma OAI.RVM.Magnetic.contDiffAt_transportAngularCore line 39
  7. lemma OAI.RVM.Magnetic.contDiffAt_coneSpatialLift line 46
  8. def OAI.RVM.Magnetic.transportSpatialFlux line 55
  9. lemma OAI.RVM.Magnetic.transportSpatialFlux_contDiffAt line 59
  10. lemma OAI.RVM.Magnetic.transportSpatialFlux_homogeneous line 71
  11. lemma OAI.RVM.Magnetic.transportSpatialFlux_angular_mean_zero line 78
  12. lemma OAI.RVM.Magnetic.transportSpatialFlux_joint_contDiffAt line 84
  13. lemma OAI.RVM.Magnetic.divergence_phase_first line 102
  14. lemma OAI.RVM.Magnetic.continuousOn_transportSpatialDivergence line 115
  15. lemma OAI.RVM.Magnetic.transportSpatialDivergence_uniform_bound line 130
  16. def OAI.RVM.Magnetic.transportConeCoefficient line 147
  17. def OAI.RVM.Magnetic.coneLorentz line 150
  18. lemma OAI.RVM.Magnetic.transportConeCoefficient_contDiffAt line 153
  19. lemma OAI.RVM.Magnetic.coneLorentz_contDiffAt line 164
  20. lemma OAI.RVM.Magnetic.coneLorentz_vlasov_before line 177
  21. lemma OAI.RVM.Magnetic.magnetic_transport_division_annulus line 186
  22. lemma OAI.RVM.Magnetic.sphere_mean_zero_lipschitz_bound line 212
  23. def OAI.RVM.Magnetic.transportSingularShell line 236
  24. lemma OAI.RVM.Magnetic.transport_divergence_sphere_continuous line 240
  25. lemma OAI.RVM.Magnetic.transportSingularShell_near_far line 251
  26. lemma OAI.RVM.Magnetic.transportSingularShell_continuousOn line 296
  27. lemma OAI.RVM.Magnetic.physical_transport_log_bound line 345
  28. lemma OAI.RVM.Magnetic.transportSpatialFlux_uniform_bound line 379
  29. lemma OAI.RVM.Magnetic.transport_sphere_rescale line 394
  30. lemma OAI.RVM.Magnetic.transport_sphere_boundary_bound line 412
  31. def OAI.RVM.Magnetic.transportVelocityProfile line 445
  32. lemma OAI.RVM.Magnetic.transportVelocityProfile_contDiffAt line 450
  33. lemma OAI.RVM.Magnetic.divergence_parameter_slice line 466
  34. lemma OAI.RVM.Magnetic.continuousOn_transportVelocityDivergence line 478
  35. lemma OAI.RVM.Magnetic.transportVelocityDivergence_uniform_bound line 492
  36. lemma OAI.RVM.Magnetic.divergence_real_const_smul line 511
  37. lemma OAI.RVM.Magnetic.transport_velocity_divergence_rescale line 520
  38. lemma OAI.RVM.Magnetic.physical_transport_velocity_bound line 539