OAI/MathematicalPhysics/Boltzmann/Branching/ReferenceAngularCharts.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

Local unit-sphere coordinates at the minorization collision

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingTangent line 15
  2. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalTangent line 16
  3. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingChart line 20
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalChart line 21
  5. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart line 22
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingChart_zero line 24
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalChart_zero line 27
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart_zero line 30
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingChart_hasFDerivAt line 33
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalChart_hasFDerivAt line 39
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingChart_contDiffAt line 48
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalChart_contDiffAt line 55
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart_contDiffAt line 62
  14. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationDerivative line 86
  15. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingChart_distance_derivative line 89
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart_hasFDerivAt line 106
  17. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialChart line 149
  18. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialDerivative line 151
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialChart_hasFDerivAt line 154
  20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialChart_contDiffAt line 163
  21. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialDerivative_injective line 167
  22. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialEquiv line 185
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialChart_hasStrictFDerivAt line 190
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalTangent_inner line 212
  25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalChart_norm line 217
  26. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSphere line 226
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSphere_measurable line 229
  28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialChart_volume_lower line 234
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalRadialChart_mem_cone line 253
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationDerivative_injective line 279
  31. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationLinearEquiv line 291
  32. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart_hasStrictFDerivAt line 296
  33. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionLocalEquiv line 301
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionLocalEquiv_function line 304
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionLocalEquiv_source line 306
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionLocalEquiv_target line 309
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionLocalEquiv_contains_ball line 314
  38. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphere_cone_volume_le line 335
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSphere_measure_bound line 347
  40. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSplit line 382
  41. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSplit_apply line 388
  42. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSplit_measurePreserving line 390
  43. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterSphere line 395
  44. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterSphere_measurable line 398
  45. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSphere_factor line 402
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSplit_map_restrict line 407
  47. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.minorizationChart_volume_lower line 441
  48. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularInterval line 487
  49. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSquare line 488
  50. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angular_box_subset_ball line 490
  51. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSquare_weighted_measure_bound line 501
  52. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularInterval_volume line 532
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereProbability_rescale line 538
  54. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.parameterSphere_dominated line 543
  55. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotationLinear line 590
  56. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotationLinear_norm line 595
  57. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotationIsometry line 603
  58. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotation line 607
  59. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotation_normal line 611
  60. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotation_second line 621
  61. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotation_tangent line 625
  62. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularRotation_normalize line 652
  63. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingParameterSphere line 656
  64. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingPatch line 659
  65. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingParameterSphere_measurable line 661
  66. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingPatch_zero line 664
  67. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingPatch_hasFDerivAt line 667
  68. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingPatch_contDiffAt line 673
  69. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingPatch_tangent line 676
  70. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incomingParameterSphere_value line 683
  71. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.paired_parameterSphere_dominated line 693
  72. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.CollisionParameters line 721
  73. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.CollisionFamilySpace line 722
  74. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionParameterBase line 724
  75. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyBase line 725
  76. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.incidentDirection line 726
  77. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamily line 728
  78. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyExtension line 730
  79. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_opposite_beam line 733
  80. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamily_slice line 738
  81. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamily_at_base line 743
  82. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyExtension_at_base line 746
  83. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.normalize_contDiffAt line 750
  84. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.child_contDiffAt line 755
  85. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.incidentDirection_contDiffAt line 762
  86. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamily_contDiffAt line 773
  87. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyExtension_contDiffAt line 803
  88. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyDerivative line 822
  89. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyExtension_hasFDerivAt line 825
  90. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyDerivative_fst line 829
  91. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyDerivative_slice line 836
  92. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyDerivative_injective line 847
  93. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyLinearEquiv line 859
  94. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyExtension_hasStrictFDerivAt line 864
  95. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyLocalEquiv line 871
  96. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyLocalEquiv_source line 874
  97. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamilyLocalEquiv_target line 877
  98. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamily_uniform line 899
  99. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionFamily_uniform_volume line 950
  100. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.angularSquare_isFinite line 981
  101. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereCollision line 988
  102. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.pairedChart line 989
  103. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.twoSphereCollision line 991
  104. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.sphereCollision_measurable line 993
  105. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.pairedChart_measurable line 997
  106. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.pairedChart_measure_le line 1001
  107. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.exists_pairedChart_measure_le line 1018
  108. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyCoordinates line 1042
  109. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyCoordinates_apply line 1046
  110. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyCoordinates_measurePreserving line 1049
  111. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.twoCollisionMap line 1053
  112. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyChart line 1056
  113. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.twoCollisionLaw line 1059
  114. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.twoCollisionMap_measurable line 1062
  115. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyChart_measurable line 1066
  116. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyChart_coordinates line 1070
  117. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyChart_measure_le line 1080
  118. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowMeasure line 1114
  119. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowMap line 1117
  120. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowMap_measurable line 1119
  121. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindowMeasure_preimage line 1123
  122. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_family_window_volume line 1135
  123. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.firstCollisionFamily line 1177
  124. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.firstCollisionFamily_at_base line 1180
  125. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.firstCollisionFamily_continuousAt line 1186
  126. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.localCollisionCore line 1197
  127. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localCollisionCore_measurable line 1199
  128. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.norm_le_two_of_near_unit line 1201
  129. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localCollisionCore_norm line 1208
  130. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.localCollisionCore_distance line 1211
  131. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beam_neighborhood_distance line 1220
  132. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.collision_window_good line 1230
  133. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.familyWindow_good line 1241