OAI/MathematicalPhysics/Boltzmann/Branching/FiveGainRank.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

The explicit nondegenerate five-collision configuration

These algebraic witnesses allow arbitrary axial cold velocities. The first three increments are independent; after the fourth increment the final two collision normals are not parallel. Derivative and analytic-null-set arguments are separate from these algebraic statements.

  1. abbrev OAI.BoltzmannNonuniqueness.FiveGainWitness.V line 33
  2. def OAI.BoltzmannNonuniqueness.FiveGainWitness.transverseSquare line 35
  3. def OAI.BoltzmannNonuniqueness.FiveGainWitness.smallFactor line 37
  4. def OAI.BoltzmannNonuniqueness.FiveGainWitness.first line 39
  5. def OAI.BoltzmannNonuniqueness.FiveGainWitness.second line 40
  6. def OAI.BoltzmannNonuniqueness.FiveGainWitness.third line 41
  7. def OAI.BoltzmannNonuniqueness.FiveGainWitness.afterThirdX line 45
  8. def OAI.BoltzmannNonuniqueness.FiveGainWitness.afterThirdY line 46
  9. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.transverseSquare_pos line 48
  10. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.smallFactor_pos line 52
  11. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.transverse_factor_pos line 57
  12. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.first_perpendicular line 69
  13. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.second_perpendicular line 72
  14. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.third_perpendicular line 75
  15. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.first_three_det line 81
  16. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.first_three_det_ne_zero line 86
  17. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.afterThird_transverse_pos line 90
  18. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.last_normals_cross_ne_zero line 98
  19. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.cross_represents line 109

    Source documentation

    Every perpendicular increment is produced by a redundant angular parameter.

    theorem cross_represents {n k : V} (hn : n ≠ 0) (hk : n ⬝ᵥ k = 0) :
    n ⨯₃ ((-(n ⬝ᵥ n)⁻¹) • (n ⨯₃ k)) = k := by
…

    Mentions: OAI.BoltzmannNonuniqueness.FiveGainWitness.V

  20. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.V line 133
  21. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.State line 134
  22. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.Parameters line 135
  23. def OAI.BoltzmannNonuniqueness.FiveGainMap.axis line 137
  24. def OAI.BoltzmannNonuniqueness.FiveGainMap.step line 139
  25. def OAI.BoltzmannNonuniqueness.FiveGainMap.path line 145

    Source documentation

    Only the first five stages change the state.

    def path (σ s : Fin 5 → ℝ) (α γ : ℝ) (z : State) (q : Parameters) : ℕ → State
  | 0 => z
  | k+1 => if h : k < 5 then
      step (σ ⟨k,h⟩) α γ (s ⟨k,h⟩) (q.1 ⟨k,h⟩) (q.2 ⟨k,h⟩)
        (path σ s α γ z q k)
    else path σ s α γ z q k

    Mentions: OAI.BoltzmannNonuniqueness.FiveGainMap.State, OAI.BoltzmannNonuniqueness.FiveGainMap.Parameters, OAI.BoltzmannNonuniqueness.FiveGainMap.step

  26. def OAI.BoltzmannNonuniqueness.FiveGainMap.map line 152
  27. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.cross_analytic line 159
  28. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.axis_analytic line 172
  29. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.step_analytic line 181
  30. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.path_analytic line 201
  31. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_analytic line 216
  32. def OAI.BoltzmannNonuniqueness.FiveGainMap.thermalCenter line 238
  33. def OAI.BoltzmannNonuniqueness.FiveGainMap.thermalStep line 241
  34. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalCenter_zero line 245
  35. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalStep_zero line 249
  36. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalCenter_analytic line 257
  37. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalStep_analytic line 281
  38. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalEnvironment line 313
  39. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalControls line 314
  40. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalInput line 315
  41. def OAI.BoltzmannNonuniqueness.FiveGainMap.thermalPath line 317
  42. def OAI.BoltzmannNonuniqueness.FiveGainMap.thermalMap line 326
  43. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalPath_zero line 329
  44. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalMap_zero line 341
  45. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalPath_analytic line 346
  46. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalMap_analytic line 373
  47. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.PositiveEnvironment line 397
  48. def OAI.BoltzmannNonuniqueness.FiveGainMap.controlDerivative line 399
  49. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalControl_hasFDerivAt line 403
  50. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalMap_compact_tendsto line 412
  51. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalDerivative_compact_tendsto line 434
  52. def OAI.BoltzmannNonuniqueness.FiveGainMap.velocityStep line 476
  53. def OAI.BoltzmannNonuniqueness.FiveGainMap.velocityPath line 478
  54. def OAI.BoltzmannNonuniqueness.FiveGainMap.commonPosition line 483
  55. def OAI.BoltzmannNonuniqueness.FiveGainMap.equalTimeSpeeds line 485
  56. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.step_same_time line 488
  57. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.path_equal_time line 493
  58. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_equal_time line 509
  59. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_equal_time_position line 516
  60. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_equal_time_position_derivative line 521
  61. def OAI.BoltzmannNonuniqueness.FiveGainWitness.endPosition line 548
  62. def OAI.BoltzmannNonuniqueness.FiveGainWitness.positionDirection line 551
  63. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.endPosition_equal_time line 554
  64. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.endPosition_hasDerivAt line 560

    Source documentation

    Dependence of the velocities contributes zero to the position derivative when all formal free-flight durations vanish.

    theorem endPosition_hasDerivAt (t₀ τ : ℝ) (x₀ v₀ : W)
    {t : ℝ → Fin 5 → ℝ} {v : ℝ → Fin 4 → W}
    {dt : Fin 5 → ℝ} {dv : Fin 4 → W}
    (ht : ∀ i, HasDerivAt (fun r => t r i) (dt i) 0)
    (hv : ∀ i, HasDerivAt (fun r => v r i) (dv i) 0)
    (heq : ∀ i, t 0 i = τ) :
    HasDerivAt (fun r => endPosition t₀ x₀ v₀ (t r) (v r))
      (positionDirection v₀ dt (v 0)) 0 := by
…

    Mentions: OAI.BoltzmannNonuniqueness.FiveGainWitness.endPosition, OAI.BoltzmannNonuniqueness.FiveGainWitness.positionDirection

  65. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.direction_first line 583
  66. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.direction_second line 587
  67. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.direction_third line 592
  68. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.path_succ_time line 614
  69. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.path_succ_position line 619
  70. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_position line 625
  71. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_position_hasDerivAt line 644
  72. def OAI.BoltzmannNonuniqueness.FiveGainMap.rotationLinear line 681
  73. def OAI.BoltzmannNonuniqueness.FiveGainMap.rotation line 690
  74. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotation_apply line 692
  75. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotation_axis line 695
  76. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotation_axial line 699
  77. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotation_cross line 701
  78. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotation_inverse line 712
  79. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotation_surjective line 722
  80. def OAI.BoltzmannNonuniqueness.FiveGainMap.rotateAngles line 743
  81. def OAI.BoltzmannNonuniqueness.FiveGainMap.rotateParameters line 746
  82. def OAI.BoltzmannNonuniqueness.FiveGainMap.rotateState line 749
  83. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotateParameters_apply line 752
  84. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotateState_apply line 755
  85. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rotateState_surjective line 758
  86. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.step_rotation line 765
  87. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.path_rotation line 779
  88. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_rotation line 794
  89. def OAI.BoltzmannNonuniqueness.FiveGainMap.positiveDomain line 816
  90. def OAI.BoltzmannNonuniqueness.FiveGainMap.timeProjection line 818
  91. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.positiveDomain_eq line 821
  92. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.positiveDomain_open line 825
  93. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.positiveDomain_convex line 829
  94. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.positiveDomain_preconnected line 835
  95. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_analyticOnNhd line 838
  96. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_derivative_analyticOnNhd line 843
  97. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.angular_pair_surjective line 865
  98. theorem OAI.BoltzmannNonuniqueness.FiveGainWitness.final_angular_surjective line 887
  99. def OAI.BoltzmannNonuniqueness.FiveGainMap.witnessVelocities line 911
  100. def OAI.BoltzmannNonuniqueness.FiveGainMap.witnessNormal line 919
  101. def OAI.BoltzmannNonuniqueness.FiveGainMap.witnessIncrement line 922
  102. def OAI.BoltzmannNonuniqueness.FiveGainMap.witnessAngles line 925
  103. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.witnessNormal_ne_zero line 929
  104. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.witness_perpendicular line 943
  105. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.witnessAngles_realize line 949
  106. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.witnessAngles_last line 954
  107. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.witness_velocityPath line 958
  108. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_at_witness line 973
  109. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.cross_hasDerivAt line 999
  110. def OAI.BoltzmannNonuniqueness.FiveGainMap.finalVelocity line 1021
  111. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.finalVelocity_hasDerivAt line 1025
  112. def OAI.BoltzmannNonuniqueness.FiveGainMap.varyLastTwo line 1050
  113. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.velocityPath_varyLastTwo line 1053
  114. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_last_angular_hasDerivAt line 1059
  115. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_time line 1090
  116. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.affineParameter_derivative line 1093
  117. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.apply_eq_of_line line 1099
  118. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_derivative_time line 1106
  119. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_derivative_position line 1120
  120. def OAI.BoltzmannNonuniqueness.FiveGainMap.lastAngularDirection line 1133
  121. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.varyLastTwo_eq line 1135
  122. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_derivative_last_angular line 1144
  123. def OAI.BoltzmannNonuniqueness.FiveGainMap.firstTimeDirection line 1183
  124. def OAI.BoltzmannNonuniqueness.FiveGainMap.witnessPosition line 1185
  125. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.witnessPosition_surjective line 1188
  126. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.positionDirection_at_witness line 1203
  127. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.surjective_of_blocks line 1229