OAI/MathematicalPhysics/Boltzmann/Branching/DoubleCollisionTests.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Surjectivity of the two-output collision variation away from grazing and parallel normals

  1. def OAI.BoltzmannNonuniqueness.CollisionCompactness.normalPlaneLift line 19
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.inner_values line 23
  3. def OAI.BoltzmannNonuniqueness.CollisionCompactness.doubleOutgoingVariation line 46

    Source documentation

    The derivative when the first normal varies through unit vectors. The normal component of its variation is included, so the formula also applies to the radially normalized extension off the sphere.

    def doubleOutgoingVariation (d n m : Velocity) (z : (Velocity × Velocity) × Velocity) :
    Velocity × Velocity :=
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity

  4. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.doubleOutgoingVariation_surjective line 52
  5. abbrev OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.Domain line 108
  6. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocityProjection line 110
  7. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.relativeProjection line 114
  8. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.normalProjection line 118
  9. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.coefficientDifferential line 121
  10. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.differential line 125
  11. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing line 130
  12. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.differential_apply line 134
  13. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.numeratorDifferential line 146
  14. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.denominatorDifferential line 149
  15. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.coefficient line 152
  16. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.numerator_hasFDerivAt line 154
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.denominator_hasFDerivAt line 167
  18. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.inverse_denominator_hasFDerivAt line 180
  19. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.coefficient_hasFDerivAt line 190
  20. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_hasFDerivAt line 205
  21. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.differential_surjective line 226
  22. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocity_line_null line 249
  23. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.normalized_parallel_mem_span line 257
  24. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.regular_normal_ae line 276
  25. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.regular_grazing_ae line 289
  26. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.scaleNormal line 312
  27. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_scale line 316
  28. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_comp_scale line 329
  29. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.scaleNormal_surjective line 334
  30. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.raw_outgoing_regular line 341
  31. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.good line 375
  32. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.good_measurable line 379
  33. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.good_ae line 392
  34. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_rank_ae line 402
  35. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.normalDomain line 432
  36. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.normalDomain_open line 434
  37. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_measurable line 437
  38. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_contDiffAt line 441
  39. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_contDiffOn line 454
  40. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_hasFDerivAt_fderiv line 457
  41. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_fderiv_continuousAt line 461
  42. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.compact_outgoing_law_absolutelyContinuous line 480
  43. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.outgoing_law_absolutelyContinuous line 516
  44. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularOutgoing line 570
  45. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularOutgoing_measurable line 573
  46. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.direction_outgoing line 576
  47. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angular_outgoing_law_absolutelyContinuous line 583
  48. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.relativePair line 638
  49. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.relativePair_measurePreserving line 640
  50. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalPairAt line 654
  51. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalPairAt_eq line 657
  52. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalPairAt_measurable line 663
  53. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalPairAt_law_absolutelyContinuous line 667
  54. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalDoubleOutgoing line 687
  55. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalDoubleOutgoing_measurable line 690
  56. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physical_double_law_absolutelyContinuous line 694
  57. abbrev OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.Parameters line 737
  58. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.incomingBall line 739
  59. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.parameterMeasure line 742
  60. instance OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.parameterMeasureFinite line 745
  61. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.rateProduct line 755
  62. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.rateProduct_measurable line 758
  63. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.rateProduct_integrable line 762
  64. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalReferenceMeasure line 787
  65. instance OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalReferenceMeasureFinite line 790
  66. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.physicalReferenceMeasure_absolutelyContinuous line 795
  67. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.referenceDensity line 824
  68. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.referenceDensity_measurable line 827
  69. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.referenceDensity_nonneg line 830
  70. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.referenceDensity_integrable line 833
  71. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.referenceDensity_integral line 842
  72. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.referenceDensity_translate line 846
  73. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.referenceDensity_test line 870
  74. def OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint line 884
  75. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_integrable line 887
  76. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_measurable line 899
  77. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.double_test_integrable line 913
  78. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.angularAdjoint_square line 927