OAI/MathematicalPhysics/Boltzmann/Model.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoltzmannNonuniqueness.Velocity line 24

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:19 (same declaration text).

2. abbrev OAI.BoltzmannNonuniqueness.Position line 25

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:20 (same declaration text).

3. abbrev OAI.BoltzmannNonuniqueness.Phase line 26

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:21 (same declaration text).

4. abbrev OAI.BoltzmannNonuniqueness.Density line 27

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:22 (same declaration text).

5. abbrev OAI.BoltzmannNonuniqueness.Sphere line 28

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:23 (same declaration text).

6. def OAI.BoltzmannNonuniqueness.sphereArea line 31

   Source documentation

   Ordinary surface area, rather than normalized probability on the sphere.

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:26 (same declaration text).

   def sphereArea : Measure Sphere := (volume : Measure Velocity).toSphere

   Mentions: OAI.BoltzmannNonuniqueness.Sphere, OAI.BoltzmannNonuniqueness.Velocity

7. def OAI.BoltzmannNonuniqueness.normalComponent line 33

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:28 (same declaration text).

8. def OAI.BoltzmannNonuniqueness.scatterLeft line 35

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:30 (same declaration text).

9. def OAI.BoltzmannNonuniqueness.scatterRight line 37

   Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:32 (same declaration text).

10. def OAI.BoltzmannNonuniqueness.collisionKernel line 39

    Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:34 (same declaration text).

11. def OAI.BoltzmannNonuniqueness.gain line 41

    Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:36 (same declaration text).

12. def OAI.BoltzmannNonuniqueness.loss line 47

    Also declared: ComparatorChallenges/BoltzmannNonuniqueness.lean:42 (same declaration text).

13. def OAI.BoltzmannNonuniqueness.collision line 52

    Distinct definitions of this name: ComparatorChallenges/BoltzmannNonuniqueness.lean:47 (same statement text; different proof or body). Qualify references as OAI.BoltzmannNonuniqueness.collision@path.

14. theorem OAI.BoltzmannNonuniqueness.collisionKernel_nonneg line 55
15. theorem OAI.BoltzmannNonuniqueness.scatter_momentum line 58
16. theorem OAI.BoltzmannNonuniqueness.scatter_energy line 63
17. theorem OAI.BoltzmannNonuniqueness.normalComponent_scatter line 71
18. theorem OAI.BoltzmannNonuniqueness.scatterLeft_involutive line 78
19. theorem OAI.BoltzmannNonuniqueness.scatterRight_involutive line 85
20. theorem OAI.BoltzmannNonuniqueness.collisionKernel_scatter line 92
21. theorem OAI.BoltzmannNonuniqueness.scatterLeft_translate line 97
22. theorem OAI.BoltzmannNonuniqueness.scatterRight_translate line 103
23. theorem OAI.BoltzmannNonuniqueness.scatter_centered_energy line 110

    Source documentation

    The center may vary with space and time: this identity is pointwise in the center.

    theorem scatter_centered_energy (v w u ω : Velocity) (hω : ‖ω‖ = 1) :
        ‖scatterLeft v w ω - u‖ ^ 2 + ‖scatterRight v w ω - u‖ ^ 2 =
          ‖v - u‖ ^ 2 + ‖w - u‖ ^ 2 := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.scatterLeft, OAI.BoltzmannNonuniqueness.scatterRight

24. def OAI.BoltzmannNonuniqueness.gaussian line 117

    Source documentation

    A Gaussian with arbitrary amplitude, exponent, and center.

    def gaussian (A β : ℝ) (u v : Velocity) : ℝ := A * Real.exp (-β * ‖v - u‖ ^ 2)

    Mentions: OAI.BoltzmannNonuniqueness.Velocity

25. theorem OAI.BoltzmannNonuniqueness.gaussian_detailed_balance line 120

    Source documentation

    Detailed balance, used for the transported Maxwellian barrier in Section 4.

    theorem gaussian_detailed_balance (A β : ℝ) (u v w ω : Velocity) (hω : ‖ω‖ = 1) :
        gaussian A β u (scatterLeft v w ω) * gaussian A β u (scatterRight v w ω) =
          gaussian A β u v * gaussian A β u w := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.gaussian, OAI.BoltzmannNonuniqueness.scatterLeft, OAI.BoltzmannNonuniqueness.scatterRight

26. theorem OAI.BoltzmannNonuniqueness.gaussian_gain_eq_loss line 136

    Source documentation

    Pointwise detailed balance proves equality of the gain and loss integrands.

    theorem gaussian_gain_eq_loss (A β : ℝ) (u : Velocity) (x : Position) (v : Velocity) :
        gain (fun z => gaussian A β u z.2) x v =
          loss (fun z => gaussian A β u z.2) x v := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.gain, OAI.BoltzmannNonuniqueness.gaussian, OAI.BoltzmannNonuniqueness.loss

27. theorem OAI.BoltzmannNonuniqueness.gaussian_collision_eq_zero line 146

    Source documentation

    This algebraic identity alone does not assert collision integrability for arbitrary β. The admissibility interface separately requires genuine finite collision integrals.

    theorem gaussian_collision_eq_zero (A β : ℝ) (u : Velocity) (x : Position)
        (v : Velocity) : collision (fun z => gaussian A β u z.2) x v = 0 := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.gaussian