OAI/MathematicalPhysics/Boltzmann/Collision/CarlemanIdentity.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

The normal-and-plane Jacobian in physical velocity coordinates

  1. def OAI.BoltzmannNonuniqueness.CarlemanCoordinates.physicalFrame line 20
  2. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.physicalFrame_measurable line 23
  3. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.transverse_norm_sq line 27
  4. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.normal_normSq line 31
  5. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.physicalFrame_map_volume line 34
  6. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.lintegral_physicalFrame line 46
  7. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.normalComponent_physicalFrame line 57
  8. def OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeFrame line 85
  9. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.axial_planeFrame line 87
  10. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.transverse_planeFrame line 90
  11. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeFrame_eq_origin_chart line 98
  12. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeFrame_orthogonal line 128
  13. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.normal_scaled line 134
  14. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.direction_pos_scaled line 139
  15. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.positive_chart_frame line 143
  16. def OAI.BoltzmannNonuniqueness.rawNonnegativeGain line 183
  17. theorem OAI.BoltzmannNonuniqueness.scatter_complement_left line 188
  18. theorem OAI.BoltzmannNonuniqueness.scatter_complement_right line 193
  19. theorem OAI.BoltzmannNonuniqueness.normal_cross_integral_symm line 198
  20. def OAI.BoltzmannNonuniqueness.rawGainIntegrand line 211
  21. theorem OAI.BoltzmannNonuniqueness.rawGainIntegrand_measurable line 214
  22. theorem OAI.BoltzmannNonuniqueness.rawGain_eq_lintegral line 228
  23. theorem OAI.BoltzmannNonuniqueness.rawNonnegativeGain_symm line 233
  24. theorem OAI.BoltzmannNonuniqueness.nonnegativeGain_eq_raw line 240
  25. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.physicalFrame_joint_measurable line 280
  26. def OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeAverage line 290
  27. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeFrame_joint_measurable line 293
  28. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeAverage_measurable line 305
  29. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeFrame_neg line 315
  30. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeAverage_neg line 321
  31. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planeAverage_eq_chart line 335
  32. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.physicalFrame_decomposition line 364
  33. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.scatterLeft_frame line 369
  34. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.scatterRight_frame line 375
  35. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.lintegral_shifted_frame line 382
  36. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.sphere_ae_transverse_ne_zero line 427
  37. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.lintegral_even_halfline line 461
  38. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.planePoint_measurable line 505
  39. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.lintegral_plane_const_mul line 510
  40. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.normal_gain_integral line 522
  41. def OAI.BoltzmannNonuniqueness.CarlemanCoordinates.radialIntegrand line 568
  42. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.radialIntegrand_measurable line 572
  43. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.radialIntegrand_neg line 584
  44. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.angularRadial_even line 592
  45. def OAI.BoltzmannNonuniqueness.CarlemanCoordinates.chartProfile line 617
  46. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.chartProfile_measurable line 620
  47. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.chartGain_eq_density_integral line 630
  48. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.radial_chart_weight line 637
  49. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.lintegral_positive_radial_weight line 663
  50. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.radial_chart_integrand line 677
  51. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.chart_integral_eq_positive_radial line 690
  52. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.rawGain_eq_signed_radial line 733
  53. theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.rawGain_eq_positive_radial line 753
  54. theorem OAI.BoltzmannNonuniqueness.nonnegativeGain_eq_chartGain line 782
  55. theorem OAI.BoltzmannNonuniqueness.Published.gpv2009CarlemanInput line 792