OAI/Analysis/VlasovMaxwell/Population/RepresentativeCosts.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.representativeClosedBin line 40
  2. lemma OAI.RVM.representativeClosedBin_radius_pos line 54
  3. lemma OAI.RVM.velocity_deficit_mem_unit2 line 60
  4. lemma OAI.RVM.physicalCutoff_positive_closedBin line 70
  5. lemma OAI.RVM.dyadicMultiFactor_le_one line 86
  6. def OAI.RVM.coneDyadicFactor line 91
  7. lemma OAI.RVM.PhaseFlowOn.coneDyadicFactor_continuousOn line 95
  8. def OAI.RVM.projectedDyadicRateKernel line 118
  9. lemma OAI.RVM.PhaseFlowOn.projectedDyadicRateKernel_continuousOn line 122
  10. lemma OAI.RVM.normalisedRatePrimitive_flux_norm line 129
  11. lemma OAI.RVM.projectedDyadicRateKernel_flux_norm line 144
  12. def OAI.RVM.physicalDyadicPrimitiveDensity line 161
  13. lemma OAI.RVM.physicalPrimitive_radius_norm line 168
  14. lemma OAI.RVM.physicalDyadicPrimitiveDensity_le line 173
  15. lemma OAI.RVM.projectedDyadicRateKernel_polar_density line 222
  16. def OAI.RVM.positiveCoordinate line 236
  17. lemma OAI.RVM.positiveCoordinate_continuous line 238
  18. lemma OAI.RVM.positiveCoordinate_norm line 241
  19. lemma OAI.RVM.positiveCoordinate_zero line 246
  20. lemma OAI.RVM.positiveCoordinate_smul line 249
  21. lemma OAI.RVM.integral_eq_of_positiveCoordinate line 254
  22. abbrev OAI.RVM.TrianglePhase line 274
  23. def OAI.RVM.trianglePhaseDomain line 276
  24. def OAI.RVM.trianglePhaseMeasure line 279
  25. def OAI.RVM.triangleKernelState line 282
  26. def OAI.RVM.triangleConeKernel line 285
  27. lemma OAI.RVM.measurableSet_trianglePhaseDomain line 292
  28. lemma OAI.RVM.PhaseFlowOn.triangleKernelState_continuousOn line 297
  29. lemma OAI.RVM.triangleKernelState_mem line 307
  30. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_measurable line 312
  31. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_lintegral_norm line 332
  32. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_integrable line 382
  33. lemma OAI.RVM.labelConeKernel_positiveCoordinate line 391
  34. lemma OAI.RVM.triangleConeKernel_positiveCoordinate line 402
  35. lemma OAI.RVM.labelConeKernel_neg line 415
  36. lemma OAI.RVM.triangleConeKernel_neg line 423
  37. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_triangle_positiveCoordinate line 431
  38. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_triangle_integral line 444
  39. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_integral line 456
  40. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_integral_sphere line 505
  41. lemma OAI.RVM.physicalDyadicPrimitiveDensity_near_pointwise line 556
  42. lemma OAI.RVM.physicalBin_triangle_weight_le line 600
  43. lemma OAI.RVM.physicalDyadicPrimitive_triangle_near line 623
  44. lemma OAI.RVM.weighted_labelProjected_congr line 691
  45. lemma OAI.RVM.PhaseFlowOn.label_projected_primitive_near line 707
  46. lemma OAI.RVM.Admissible.label_projected_primitive_near_constant line 765
  47. lemma OAI.RVM.finset_subset_dyadicBox line 791
  48. def OAI.RVM.directionWeightMajorant line 802
  49. lemma OAI.RVM.directionWeightMajorant_nonneg line 806
  50. lemma OAI.RVM.sum_range_indicator_lt line 811
  51. lemma OAI.RVM.sum_directionWeightMajorant_box line 820
  52. lemma OAI.RVM.sum_directionWeightMajorant line 846
  53. lemma OAI.RVM.tsum_directionWeightMajorant line 852
  54. lemma OAI.RVM.selected_representative_weight_bound line 859
  55. lemma OAI.RVM.selectedDyadicCutoff_ofReal line 892
  56. lemma OAI.RVM.PhaseFlowOn.label_projected_dyadic_eq line 919
  57. lemma OAI.RVM.PhaseFlowOn.selected_receiver_rate_norm_sum line 935
  58. lemma OAI.RVM.sourceRepresentative_le_four line 1006
  59. lemma OAI.RVM.cappedRepresentative_le_four line 1014
  60. lemma OAI.RVM.dyadicSelectionBoundary_direction line 1022
  61. lemma OAI.RVM.representativeClosedBin_small_of_angle line 1066
  62. lemma OAI.RVM.dyadicSelectionBoundary_small line 1073
  63. lemma OAI.RVM.relaxed_representative_moving_bound line 1085
  64. def OAI.RVM.receiverBoundaryBinCost line 1117
  65. lemma OAI.RVM.Admissible.receiver_cutoff_boundary_sum line 1123