OAI/Analysis/VlasovMaxwell/Flow/WithinFlow.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.spaceDerivative line 30
  2. lemma OAI.RVM.hasFDerivAt_time_slice line 33
  3. lemma OAI.RVM.contDiffOn_spaceDerivative line 41
  4. def OAI.RVM.withinVariationalField line 52
  5. lemma OAI.RVM.contDiffOn_withinVariationalField line 56
  6. lemma OAI.RVM.continuousOn_time_label_of_lipschitz line 73
  7. lemma OAI.RVM.hasStrictFDerivAt_time_flow line 95
  8. lemma OAI.RVM.withinVariationalField_bounded line 125
  9. lemma OAI.RVM.exists_within_variational_flow line 144
  10. lemma OAI.RVM.hasFDerivAt_within_variational_flow line 225
  11. lemma OAI.RVM.flow_injOn_of_within_ode line 297
  12. lemma OAI.RVM.exists_bounded_within_variational_flow line 329
  13. lemma OAI.RVM.exists_bounded_within_volume_flow line 390
  14. lemma OAI.RVM.exists_bounded_within_volume_flow_joint line 417
  15. lemma OAI.RVM.cutLorentz_regular_slab line 457
  16. lemma OAI.RVM.cutLorentz_bounded_slab line 473
  17. lemma OAI.RVM.cross_smul_right line 506
  18. lemma OAI.RVM.cutLorentz_eq_lorentzPhase line 510
  19. lemma OAI.RVM.trace_cutLorentz_slab line 516
  20. lemma OAI.RVM.exists_finite_lorentz_within_volume_flow line 526
  21. lemma OAI.RVM.eqOn_of_within_ode line 588
  22. lemma OAI.RVM.contDiffOn_lorentzField_slab line 631
  23. lemma OAI.RVM.exists_lorentz_ode_on_slab line 644
  24. lemma OAI.RVM.exists_global_lorentz_flow_on_slab line 672
  25. def OAI.RVM.timeFlowDerivative line 740
  26. lemma OAI.RVM.timeFlowDerivative_det line 744
  27. lemma OAI.RVM.inverse_timeFlowDerivative line 752
  28. def OAI.RVM.inversePhase line 797
  29. lemma OAI.RVM.hasStrictFDerivAt_inversePhase line 799
  30. lemma OAI.RVM.determinant_retarded_graph line 831
  31. lemma OAI.RVM.hasStrictFDerivAt_norm_nonzero line 850
  32. def OAI.RVM.coneCovector line 867
  33. lemma OAI.RVM.coneCovector_apply line 870
  34. lemma OAI.RVM.hasStrictFDerivAt_retarded_time line 875
  35. lemma OAI.RVM.norm_coneDirection line 885
  36. lemma OAI.RVM.cone_deficit_positive line 889
  37. lemma OAI.RVM.measurePreserving_of_bijective_det_one line 919
  38. lemma OAI.RVM.integral_eq_integral_comp_of_bijective_det_one line 932
  39. structure OAI.RVM.PhaseFlowOn line 942
  40. lemma OAI.RVM.exists_phaseFlowOn line 955
  41. instance OAI.RVM.phaseVolume_isAddHaarMeasure line 963
  42. lemma OAI.RVM.PhaseFlowOn.measurePreserving line 967
  43. lemma OAI.RVM.PhaseFlowOn.integral_comp line 972
  44. lemma OAI.RVM.PhaseFlowOn.continuousOn_time line 982
  45. lemma OAI.RVM.PhaseFlowOn.timelike line 986
  46. lemma OAI.RVM.PhaseFlowOn.emission_strictMono line 998
  47. lemma OAI.RVM.PhaseFlowOn.inversePhase_flow line 1013
  48. lemma OAI.RVM.PhaseFlowOn.flow_inversePhase line 1017
  49. lemma OAI.RVM.PhaseFlowOn.tip_null line 1021
  50. def OAI.RVM.retardedLabel line 1036
  51. lemma OAI.RVM.PhaseFlowOn.inverse_differential line 1039
  52. lemma OAI.RVM.PhaseFlowOn.retarded_differential line 1051
  53. lemma OAI.RVM.PhaseFlowOn.retarded_jacobian line 1067
  54. lemma OAI.RVM.PhaseFlowOn.retarded_jacobian_pos line 1075