OAI/Analysis/VlasovMaxwell/Regularity/CurvatureBounds.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.CurvatureBound line 16
  2. lemma OAI.RVM.taylor_remainder_of_fderiv_lipschitz line 20
  3. lemma OAI.RVM.curvature_of_fderiv_lipschitz line 33
  4. lemma OAI.RVM.smooth_compact_curvature line 46
  5. lemma OAI.RVM.CurvatureBound.triple line 54
  6. lemma OAI.RVM.CurvatureBound.comp line 80
  7. lemma OAI.RVM.inverse_q_lipschitz line 101
  8. lemma OAI.RVM.velocityProjection_parameter_lipschitz line 108
  9. lemma OAI.RVM.fderiv_velocity_lipschitz line 125
  10. lemma OAI.RVM.velocity_curvature line 153
  11. lemma OAI.RVM.CurvatureBound.precomp_linear line 159
  12. lemma OAI.RVM.CurvatureBound.add line 169
  13. lemma OAI.RVM.CurvatureBound.cross_product line 179
  14. lemma OAI.RVM.lorentzField_curvature line 209
  15. def OAI.RVM.SmoothLorentzFlow.reversePath line 247
  16. lemma OAI.RVM.SmoothLorentzFlow.reversePath_deriv line 250
  17. lemma OAI.RVM.SmoothLorentzFlow.reversePath_zero line 258
  18. lemma OAI.RVM.SmoothLorentzFlow.reversePath_end line 262
  19. lemma OAI.RVM.SmoothLorentzFlow.reversePath_lipschitz line 266
  20. lemma OAI.RVM.SmoothLorentzFlow.backward_curvature line 289
  21. lemma OAI.RVM.CurvatureBound.mono line 355
  22. lemma OAI.RVM.CurvatureBound.prodMk line 360
  23. lemma OAI.RVM.CurvatureBound.translate line 368
  24. lemma OAI.RVM.transported_curvature line 377
  25. lemma OAI.RVM.CurvatureBound.neg line 404
  26. lemma OAI.RVM.CurvatureBound.sub line 410
  27. lemma OAI.RVM.CurvatureBound.const_smul line 416
  28. lemma OAI.RVM.CurvatureBound.post_linear line 425
  29. lemma OAI.RVM.CurvatureBound.coordinate line 434
  30. lemma OAI.RVM.CurvatureBound.spatial_slice line 440
  31. lemma OAI.RVM.CurvatureBound.clm_apply_const line 446
  32. lemma OAI.RVM.CurvatureBound.integral line 455
  33. lemma OAI.RVM.curvature_of_second_derivative_bound line 467
  34. lemma OAI.RVM.BoundedSmooth.spatial_curvature line 478
  35. lemma OAI.RVM.CurvatureBound.smul_const line 492
  36. lemma OAI.RVM.sphere_average_curvature line 501
  37. lemma OAI.RVM.uniform_datum_velocity_integral_curvature line 512
  38. lemma OAI.RVM.freeWave_curvature line 544
  39. lemma OAI.RVM.waveK_curvature line 570
  40. lemma OAI.RVM.CurvatureBound.curl_coordinate line 583
  41. lemma OAI.RVM.BoundedSmooth.freeWave_coordinate_curvature line 596
  42. lemma OAI.RVM.CurvatureBound.dot_const line 625
  43. lemma OAI.RVM.datum_moment_curvature line 633
  44. lemma OAI.RVM.datum_sphere_flux_curvature line 645
  45. lemma OAI.RVM.weighted_sphere_mean_curvature line 670
  46. lemma OAI.RVM.electricConeBoundary_datum_curvature line 684
  47. lemma OAI.RVM.magneticConeBoundary_datum_curvature line 711
  48. lemma OAI.RVM.datum_boundary_global_curvature line 747
  49. lemma OAI.RVM.variable_integral_gronwall_bound line 790
  50. lemma OAI.RVM.variable_integral_gronwall_bound_on line 831
  51. lemma OAI.RVM.norm_ode_volterra_bound line 861
  52. lemma OAI.RVM.backward_norm_ode_volterra_bound line 884
  53. lemma OAI.RVM.transport_on_characteristic_before line 912
  54. lemma OAI.RVM.continuousOn_lorentz_along line 933
  55. lemma OAI.RVM.characteristic_separation_volterra line 944
  56. lemma OAI.RVM.particle_lipschitz_volterra_before line 964
  57. lemma OAI.RVM.admissible_particle_lipschitz line 995
  58. lemma OAI.RVM.particle_gradient_volterra_before line 1006
  59. lemma OAI.RVM.norm_ode_inhomogeneous_bound line 1042
  60. lemma OAI.RVM.backward_norm_ode_uniform_bound line 1075
  61. lemma OAI.RVM.backward_norm_ode_inhomogeneous_bound line 1097
  62. lemma OAI.RVM.exists_phase_characteristic_before line 1120
  63. lemma OAI.RVM.characteristic_separation_uniform line 1135
  64. lemma OAI.RVM.characteristic_curvature_volterra line 1152
  65. lemma OAI.RVM.particle_curvature_volterra_before line 1207
  66. lemma OAI.RVM.CurvatureBound.fderiv_lipschitz line 1242
  67. lemma OAI.RVM.CurvatureBound.second_derivative_bound line 1331