OAI/Analysis/VlasovMaxwell/Geometry/ClosedBranchDomain.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.closedBranchDomain line 38
  2. lemma OAI.RVM.PhaseFlowOn.branch_spec_closed line 41
  3. lemma OAI.RVM.PhaseFlowOn.branch_unique_closed line 56
  4. lemma OAI.RVM.PhaseFlowOn.closedBranchDomain_eq line 66
  5. lemma OAI.RVM.PhaseFlowOn.branchDomain_eq line 84
  6. lemma OAI.RVM.PhaseFlowOn.branch_final_endpoint line 102
  7. lemma OAI.RVM.PhaseFlowOn.branch_lipschitzOn_closed line 110
  8. lemma OAI.RVM.PhaseFlowOn.branch_radius_pos_closed line 153
  9. lemma OAI.RVM.PhaseFlowOn.branchDirection_norm_closed line 165
  10. lemma OAI.RVM.PhaseFlowOn.acceleration_continuousOn_closed line 176
  11. lemma OAI.RVM.continuousOn_retardedPrimitive line 192
  12. lemma OAI.RVM.PhaseFlowOn.actual_signed_identity_closed line 210
  13. def OAI.RVM.labelBranchDomain line 326
  14. lemma OAI.RVM.labelBranchDomain_iff line 329
  15. lemma OAI.RVM.PhaseFlowOn.arrivalTime_flow_eq_branchTime line 337
  16. def OAI.RVM.actualLabelSignedForce line 344
  17. lemma OAI.RVM.PhaseFlowOn.actualLabelSignedForce_eq_pullback line 352
  18. lemma OAI.RVM.PhaseFlowOn.measurable_actualLabelSignedForce line 371
  19. lemma OAI.RVM.PhaseFlowOn.actualLabelSignedForce_integrable line 377
  20. lemma OAI.RVM.PhaseFlowOn.label_signed_integral_fubini line 384
  21. def OAI.RVM.normalisedPrimitive line 391
  22. lemma OAI.RVM.normalisedPrimitive_eq line 394
  23. def OAI.RVM.normalisedRemainder line 400
  24. lemma OAI.RVM.normalisedRemainder_eq line 404
  25. lemma OAI.RVM.continuousOn_normalisedPrimitive line 409
  26. lemma OAI.RVM.continuousOn_normalisedRemainder line 422
  27. lemma OAI.RVM.PhaseFlowOn.normalised_primitive_continuousOn line 440
  28. lemma OAI.RVM.PhaseFlowOn.normalised_remainder_continuousOn line 456
  29. def OAI.RVM.labelKernelState line 474
  30. def OAI.RVM.labelConeKernel line 477
  31. lemma OAI.RVM.PhaseFlowOn.labelKernelState_eq_arrival line 482
  32. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_eq_pullback line 489
  33. lemma OAI.RVM.PhaseFlowOn.measurable_labelConeKernel line 507
  34. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_integrable line 514
  35. def OAI.RVM.actualLabelPrimitive line 522
  36. def OAI.RVM.actualLabelRemainder line 528
  37. lemma OAI.RVM.PhaseFlowOn.actualLabelPrimitive_eq_normalised line 535
  38. lemma OAI.RVM.PhaseFlowOn.actualLabelRemainder_eq_normalised line 550
  39. lemma OAI.RVM.PhaseFlowOn.actualLabelPrimitive_integrable line 565
  40. lemma OAI.RVM.PhaseFlowOn.actualLabelPrimitive_measurable line 571
  41. lemma OAI.RVM.PhaseFlowOn.actualLabelRemainder_integrable line 577
  42. lemma OAI.RVM.PhaseFlowOn.actualLabelRemainder_measurable line 583