OAI/Analysis/VlasovMaxwell/Population/PhysicalBinPhaseSet.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.measurableSet_coneMomentumFiber line 39
  2. def OAI.RVM.physicalBinPhaseSet line 51
  3. lemma OAI.RVM.measurableSet_physicalBinPhaseSet line 54
  4. lemma OAI.RVM.physicalBinPhase_integral line 60
  5. lemma OAI.RVM.stateCutoff_derivative_physical_cover line 83
  6. lemma OAI.RVM.physicalBinPhase_cover_lintegral line 99
  7. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_measurable_interior line 135
  8. def OAI.RVM.partialCutoffTriangle line 155
  9. lemma OAI.RVM.partialCutoffTriangle_of_mem line 161
  10. lemma OAI.RVM.partialCutoffTriangle_of_notMem line 168
  11. lemma OAI.RVM.PhaseFlowOn.partialCutoffTriangle_measurable line 174
  12. lemma OAI.RVM.PhaseFlowOn.partialCutoffTriangle_support line 185
  13. lemma OAI.RVM.PhaseFlowOn.partialCutoffTriangle_boundary_sum line 223
  14. lemma OAI.RVM.normalised_partial_kernel_eq line 245
  15. def OAI.RVM.coneReceiverCutoffTangent line 253
  16. lemma OAI.RVM.PhaseFlowOn.coneReceiverCutoffTangent_continuousOn line 257
  17. lemma OAI.RVM.PhaseFlowOn.partialCutoffTriangle_receiver_density_le line 263
  18. lemma OAI.RVM.Admissible.actual_receiverCutoff_triangle_bound line 311
  19. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_lintegral_norm_measurable line 354
  20. lemma OAI.RVM.partialCutoffTriangle_eq_kernel line 404
  21. lemma OAI.RVM.PhaseFlowOn.partialCutoffLabelCost_triangle line 417
  22. lemma OAI.RVM.coneReceiverCutoffTangent_pullback line 431
  23. lemma OAI.RVM.Admissible.actual_receiverCutoff_label_bound line 438
  24. def OAI.RVM.coneSourceCutoffTangent line 466
  25. def OAI.RVM.coneGeometryCutoffTangent line 470
  26. lemma OAI.RVM.PhaseFlowOn.coneSourceCutoffTangent_continuousOn line 474
  27. lemma OAI.RVM.PhaseFlowOn.coneGeometryCutoffTangent_continuousOn line 480
  28. lemma OAI.RVM.coneSourceCutoffTangent_pullback line 487
  29. lemma OAI.RVM.coneGeometryCutoffTangent_pullback line 492
  30. lemma OAI.RVM.PhaseFlowOn.partialCutoffTriangle_source_density_le line 499
  31. lemma OAI.RVM.PhaseFlowOn.partialCutoffTriangle_geometry_density_le line 548
  32. lemma OAI.RVM.PhaseFlowOn.actual_sourceCutoff_label_boundary_sum line 595
  33. lemma OAI.RVM.PhaseFlowOn.actual_geometryCutoff_label_boundary_sum line 629