OAI/Analysis/VlasovMaxwell/Population/DyadicCut.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.dyadicCut line 34
  2. def OAI.RVM.dyadicBump line 35
  3. def OAI.RVM.dyadicFactor line 36
  4. lemma OAI.RVM.contDiff_dyadicCut line 38
  5. lemma OAI.RVM.contDiff_dyadicBump line 40
  6. lemma OAI.RVM.contDiff_dyadicFactor line 42
  7. lemma OAI.RVM.dyadicCut_one line 45
  8. lemma OAI.RVM.dyadicCut_zero line 47
  9. lemma OAI.RVM.dyadicCut_antitone line 49
  10. lemma OAI.RVM.dyadicCut_nonneg line 52
  11. lemma OAI.RVM.dyadicCut_le_one line 53
  12. lemma OAI.RVM.dyadicBump_zero_left line 54
  13. lemma OAI.RVM.dyadicBump_zero_right line 56
  14. lemma OAI.RVM.dyadicBump_nonneg line 58
  15. lemma OAI.RVM.dyadicBump_le_one line 62
  16. lemma OAI.RVM.dyadicBump_support line 64
  17. lemma OAI.RVM.compactSupport_dyadicBump line 72
  18. lemma OAI.RVM.dyadicFactor_nonneg line 74
  19. lemma OAI.RVM.dyadicFactor_le_one line 75
  20. lemma OAI.RVM.dyadicFactor_eq line 77
  21. lemma OAI.RVM.sum_dyadicFactor line 82
  22. lemma OAI.RVM.dyadicFactor_zero_large line 88
  23. lemma OAI.RVM.dyadicFactor_eventually_zero line 91
  24. lemma OAI.RVM.dyadicFactor_locally_finite line 100
  25. lemma OAI.RVM.tsum_dyadicFactor line 107
  26. lemma OAI.RVM.hasDerivAt_dyadicFactor line 128
  27. lemma OAI.RVM.dyadicFactor_log_derivative_bound line 135
  28. def OAI.RVM.DyadicBand line 150
  29. lemma OAI.RVM.dyadicFactor_tsupport line 152
  30. lemma OAI.RVM.dyadicBand_index_le line 165
  31. lemma OAI.RVM.dyadicBand_card_le line 179
  32. lemma OAI.RVM.hasDerivAt_dyadicCut_zero_left line 227
  33. lemma OAI.RVM.hasDerivAt_dyadicCut_zero_right line 234
  34. lemma OAI.RVM.hasDerivAt_sum_dyadicFactor_zero line 241
  35. def OAI.RVM.dyadicMultiFactor line 248
  36. def OAI.RVM.dyadicBox line 251
  37. lemma OAI.RVM.dyadicMultiFactor_nonneg line 254
  38. lemma OAI.RVM.sum_dyadicMultiFactor line 257
  39. lemma OAI.RVM.sum_dyadicMultiFactor_eq_one line 265
  40. lemma OAI.RVM.differentiableAt_dyadicMultiFactor_curve line 271
  41. lemma OAI.RVM.hasDerivAt_sum_dyadicMultiFactor_zero line 278
  42. lemma OAI.RVM.selected_dyadic_derivative_cancel line 289
  43. lemma OAI.RVM.selected_dyadic_derivative_boundary line 304
  44. lemma OAI.RVM.dyadicMultiFactor_positive_bands line 331
  45. lemma OAI.RVM.dyadicMultiFactor_positive_index_comparison line 341