OAI/Analysis/VlasovMaxwell/Regularity/SmoothIntegral.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.contDiff_iteratedFDeriv_slice line 16
  2. def OAI.RVM.SmoothCompactFamily line 43
  3. lemma OAI.RVM.SmoothCompactFamily.ofJoint line 47
  4. lemma OAI.RVM.SmoothCompactFamily.continuous line 54
  5. lemma OAI.RVM.SmoothCompactFamily.derivFamily line 59
  6. lemma OAI.RVM.hasFDerivAt_integral_smoothFamily line 72
  7. lemma OAI.RVM.contDiff_integral_smoothFamily_nat line 89
  8. lemma OAI.RVM.contDiff_integral_smoothFamily line 110
  9. lemma OAI.RVM.norm_iteratedFDeriv_integral_le line 115
  10. lemma OAI.RVM.norm_iteratedFDeriv_intervalIntegral_le line 139
  11. lemma OAI.RVM.contDiff_spatial_intervalIntegral line 161
  12. lemma OAI.RVM.integral_gronwall_bound line 174