OAI/Analysis/VlasovMaxwell/Population/MomentumDirection.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.dyadicFactor_curve_log_bound line 37
  2. lemma OAI.RVM.dyadicMultiFactor_curve_zero_derivative line 50
  3. lemma OAI.RVM.dyadicMultiFactor_curve_log_bound line 60
  4. lemma OAI.RVM.dyadicMultiFactor_curve_indicator_bound line 85
  5. lemma OAI.RVM.selected_dyadic_derivative_indicator_bound line 104
  6. def OAI.RVM.momentumDirection line 119
  7. lemma OAI.RVM.momentumDirection_norm line 121
  8. lemma OAI.RVM.hasDerivAt_momentumDirection line 124
  9. def OAI.RVM.angularMultiplier line 137
  10. lemma OAI.RVM.hasDerivAt_angularMultiplier line 140
  11. lemma OAI.RVM.angularMultiplier_derivative_bound line 161
  12. lemma OAI.RVM.dyadicBand_multi_card_le line 187
  13. lemma OAI.RVM.selectedDyadicCutoff_uniform_log_bound line 205
  14. lemma OAI.RVM.selectedDyadicCutoff_mem_unit line 240
  15. lemma OAI.RVM.physical_cutoff_logarithmic_rates line 255
  16. def OAI.RVM.sourceRepresentative line 335
  17. def OAI.RVM.cappedRepresentative line 337
  18. lemma OAI.RVM.dyadicBand_capped_range line 339
  19. lemma OAI.RVM.dyadicBand_source_range line 350
  20. lemma OAI.RVM.sourceRepresentative_mem_range line 360
  21. lemma OAI.RVM.dyadicBand_angular_range line 369
  22. lemma OAI.RVM.dyadicBand_radius_range line 380
  23. lemma OAI.RVM.PhaseFlowOn.retardedMomentum_hasDerivAt line 389
  24. lemma OAI.RVM.PhaseFlowOn.actual_cutoff_logarithmic_rates line 407
  25. def OAI.RVM.transverseCLM line 431
  26. lemma OAI.RVM.transverseCLM_apply line 435
  27. def OAI.RVM.angularMultiplierCLM line 440
  28. lemma OAI.RVM.angularMultiplierCLM_apply line 442
  29. lemma OAI.RVM.contDiffAt_transverseCLM line 446
  30. lemma OAI.RVM.contDiffAt_angularMultiplierCLM line 452
  31. def OAI.RVM.angularDerivativeCLM line 457
  32. lemma OAI.RVM.angularDerivativeCLM_apply line 463
  33. lemma OAI.RVM.hasDerivAt_angularMultiplierCLM line 471
  34. lemma OAI.RVM.angularDerivativeCLM_norm_le line 484
  35. lemma OAI.RVM.continuousOn_momentumDirection line 491
  36. lemma OAI.RVM.continuousOn_transverseCLM line 496
  37. lemma OAI.RVM.continuousOn_transverseProjection line 502
  38. lemma OAI.RVM.continuousOn_realTensor line 507
  39. lemma OAI.RVM.continuousOn_angularDerivativeCLM line 516
  40. lemma OAI.RVM.sourceRepresentative_sum_bound line 581