OAI/Analysis/VlasovMaxwell/LocalPDE/VlasovConstruction.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.contDiff_spaceDerivative line 19
  2. lemma OAI.RVM.smooth_ode_unique line 29
  3. def OAI.RVM.BoundedFlowRegularity line 61
  4. lemma OAI.RVM.bounded_cutoff_vector_field line 73
  5. lemma OAI.RVM.contDiffAt_flow_transfer line 99
  6. lemma OAI.RVM.boundedFlowRegularity_zero line 129
  7. lemma OAI.RVM.boundedFlowRegularity_succ line 146
  8. lemma OAI.RVM.boundedFlowRegularity_all line 218
  9. lemma OAI.RVM.contDiffOn_bounded_flow line 223
  10. lemma OAI.RVM.PhaseFlowOn.contDiffOn_joint line 238
  11. lemma OAI.RVM.contDiffAt_inversePhase line 261
  12. lemma OAI.RVM.PhaseFlowOn.contDiffOn_inverse line 295
  13. structure OAI.RVM.SymmetricLorentzFlow line 310
  14. lemma OAI.RVM.exists_symmetricLorentzFlow line 322
  15. lemma OAI.RVM.smooth_ode_unique_Icc line 374
  16. lemma OAI.RVM.SymmetricLorentzFlow.agree line 404
  17. lemma OAI.RVM.SymmetricLorentzFlow.backward_agree line 422
  18. structure OAI.RVM.SmoothLorentzFlow line 435
  19. lemma OAI.RVM.exists_smoothLorentzFlow line 445
  20. def OAI.RVM.SmoothLorentzFlow.particle line 495
  21. lemma OAI.RVM.SmoothLorentzFlow.contDiff_particle line 497
  22. lemma OAI.RVM.SmoothLorentzFlow.particle_along line 500
  23. lemma OAI.RVM.SmoothLorentzFlow.backward_initial line 504
  24. lemma OAI.RVM.SmoothLorentzFlow.particle_initial line 507
  25. lemma OAI.RVM.SmoothLorentzFlow.particle_nonneg line 510
  26. lemma OAI.RVM.SmoothLorentzFlow.particle_compact line 513
  27. lemma OAI.RVM.SmoothLorentzFlow.particle_vlasov_direction line 524
  28. lemma OAI.RVM.SmoothLorentzFlow.particle_vlasov line 539
  29. lemma OAI.RVM.SmoothLorentzFlow.particle_vlasov_within line 549
  30. lemma OAI.RVM.SmoothLorentzFlow.particle_local_data line 561
  31. lemma OAI.RVM.SmoothLorentzFlow.moment_smooth line 575
  32. lemma OAI.RVM.SmoothLorentzFlow.rho_smooth line 589
  33. lemma OAI.RVM.SmoothLorentzFlow.current_smooth line 595
  34. lemma OAI.RVM.SmoothLorentzFlow.particle_moment_integrable line 599
  35. lemma OAI.RVM.SmoothLorentzFlow.current_component line 610
  36. lemma OAI.RVM.SmoothLorentzFlow.source_conservation line 618
  37. lemma OAI.RVM.waveK_congr_sphere line 655
  38. lemma OAI.RVM.waveK_zero_of_sphere line 662
  39. lemma OAI.RVM.norm_sub_radius_le line 667
  40. lemma OAI.RVM.waveK_zero_outside line 673
  41. lemma OAI.RVM.sourceWave_zero_outside line 678
  42. lemma OAI.RVM.sourceField_zero_outside line 691
  43. lemma OAI.RVM.sourceField_zero line 698
  44. lemma OAI.RVM.freeField_velocity_congr line 702
  45. lemma OAI.RVM.fderiv_zero_outside_spatial line 711
  46. lemma OAI.RVM.waveGradient_zero_outside line 723
  47. lemma OAI.RVM.spaceCurl_zero_outside line 730
  48. lemma OAI.RVM.SmoothLorentzFlow.source_spatial_support line 738
  49. lemma OAI.RVM.maxwell_perturbation_zero_outside line 755
  50. lemma OAI.RVM.TimeContinuousL2.add line 803
  51. lemma OAI.RVM.timeContinuousL2_congr line 812
  52. lemma OAI.RVM.timeContinuousL2_compact line 818
  53. lemma OAI.RVM.maxwell_timeContinuousL2 line 840
  54. def OAI.RVM.MaxwellFor line 874
  55. def OAI.RVM.TransportFor line 879
  56. theorem OAI.RVM.exists_picard_step line 882
  57. lemma OAI.RVM.equations_of_maxwell_transport line 917