OAI/Analysis/VlasovMaxwell/Regularity/SpatialJets.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.SpatiallySmoothSlab line 17
  2. lemma OAI.RVM.spatiallySmoothSlab_of_uniform_jets line 23
  3. theorem OAI.RVM.exists_local_spatially_smooth_classical line 37
  4. def OAI.RVM.SpatialJetRegular line 88
  5. lemma OAI.RVM.SpatiallySmoothSlab.spatialJetRegular line 97
  6. lemma OAI.RVM.SpatialJetRegular.regular line 101
  7. lemma OAI.RVM.SpatialJetRegular.deriv line 106
  8. lemma OAI.RVM.SpatialJetRegular.clm line 116
  9. lemma OAI.RVM.SpatialJetRegular.add line 125
  10. lemma OAI.RVM.SpatialJetRegular.congr line 133
  11. lemma OAI.RVM.spatialJetRegular_bilinear_jet line 141
  12. lemma OAI.RVM.SpatialJetRegular.bilinear line 182
  13. lemma OAI.RVM.spatialJetRegular_iterated line 194
  14. lemma OAI.RVM.SpatialJetRegular.mono_order line 210
  15. lemma OAI.RVM.SpatialJetRegular.precomp line 221
  16. lemma OAI.RVM.spatialJetRegular_fixed line 233
  17. lemma OAI.RVM.SpatialJetRegular.neg line 239
  18. lemma OAI.RVM.SpatialJetRegular.sub line 243
  19. lemma OAI.RVM.SpatialJetRegular.prodMk line 247
  20. lemma OAI.RVM.SpatialJetRegular.clm_comp_const line 254
  21. lemma OAI.RVM.SpatialJetRegular.clm_apply line 259
  22. lemma OAI.RVM.hasFDerivWithinAt_integral_dominated line 270
  23. lemma OAI.RVM.hasFDerivWithinAt_integral_compactFamily line 332
  24. lemma OAI.RVM.contDiffOn_integral_compact_parameter_nat line 375
  25. lemma OAI.RVM.contDiffOn_integral_spatialJet line 427
  26. lemma OAI.RVM.spatialJet_compactFamily line 442
  27. lemma OAI.RVM.fderiv_integral_spatialJet line 452
  28. lemma OAI.RVM.spatialJetRegular_integral_jet line 467
  29. lemma OAI.RVM.SpatialJetRegular.integral_compact line 498
  30. lemma OAI.RVM.SpatialJetRegular.compactTimeFamily line 516
  31. lemma OAI.RVM.SpatialJetRegular.hasFDerivAt_timeIntegral line 527
  32. lemma OAI.RVM.space_time_derivative_interval line 546
  33. lemma OAI.RVM.space_time_derivative_open line 585
  34. lemma OAI.RVM.space_time_derivative_slab line 598