CollisionMeasure.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

Measure preservation for a hard-sphere collision

For each fixed unit normal, the pre/post-collisional map is an orthogonal involution on the six-dimensional velocity-pair space. Its Euclidean norm is implemented with WithLp 2; the final measure statement uses the ordinary product of the two three-dimensional Lebesgue measures.

def OAI.BoltzmannNonuniqueness.scatterPair line 26
Source documentation
The pre/post-collisional map, with the collision normal fixed.
```
def scatterPair (ω : Velocity) (p : Velocity × Velocity) : Velocity × Velocity :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.scatterPair_involutive line 29
def OAI.BoltzmannNonuniqueness.scatterLinearMap line 36
Source documentation
Linearity holds even before imposing the unit-normal condition.
```
def scatterLinearMap (ω : Velocity) :
    (Velocity × Velocity) →ₗ[ℝ] (Velocity × Velocity) where
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
def OAI.BoltzmannNonuniqueness.scatterLinearEquiv line 57
Source documentation
A unit-normal collision is a linear involution.
```
def scatterLinearEquiv (ω : Velocity) (hω : ‖ω‖ = 1) :
    (Velocity × Velocity) ≃ₗ[ℝ] (Velocity × Velocity) :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
abbrev OAI.BoltzmannNonuniqueness.EuclideanVelocityPair line 62
Source documentation
The Euclidean velocity-pair space, whose norm squared is total kinetic energy.
```
abbrev EuclideanVelocityPair := WithLp 2 (Velocity × Velocity)
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
def OAI.BoltzmannNonuniqueness.scatterEuclideanLinearEquiv line 65
Source documentation
The collision linear equivalence transported to the Euclidean pair norm.
```
def scatterEuclideanLinearEquiv (ω : Velocity) (hω : ‖ω‖ = 1) :
    EuclideanVelocityPair ≃ₗ[ℝ] EuclideanVelocityPair :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.EuclideanVelocityPair
theorem OAI.BoltzmannNonuniqueness.scatterEuclideanLinearEquiv_apply line 70
def OAI.BoltzmannNonuniqueness.scatterLinearIsometryEquiv line 76
Source documentation
Conservation of total kinetic energy makes the collision map an isometry.
```
def scatterLinearIsometryEquiv (ω : Velocity) (hω : ‖ω‖ = 1) :
    EuclideanVelocityPair ≃ₗᵢ[ℝ] EuclideanVelocityPair where
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.EuclideanVelocityPair
theorem OAI.BoltzmannNonuniqueness.scatterPair_measurePreserving line 85
Source documentation
Fixed-normal pre/post collision change of variables preserves product Lebesgue measure.
```
theorem scatterPair_measurePreserving (ω : Velocity) (hω : ‖ω‖ = 1) :
    MeasurePreserving (scatterPair ω)
      ((volume : Measure Velocity).prod volume)
      ((volume : Measure Velocity).prod volume) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.scatterPair
theorem OAI.BoltzmannNonuniqueness.scatterPair_measurableEmbedding line 94

theorem OAI.BoltzmannNonuniqueness.integral_scatterPair line 99

Source documentation

The unweighted pre/post-collisional change-of-variables identity.

theorem integral_scatterPair (ω : Velocity) (hω : ‖ω‖ = 1)
    (F : Velocity × Velocity → ℝ) :
    (∫ p, F (scatterPair ω p) ∂((volume : Measure Velocity).prod volume)) =
      ∫ p, F p ∂((volume : Measure Velocity).prod volume) :=
…

Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.scatterPair

theorem OAI.BoltzmannNonuniqueness.integral_collisionKernel_scatterPair line 107

Source documentation

The hard-sphere angular factor is unchanged by the pre/post change of variables.

theorem integral_collisionKernel_scatterPair (ω : Velocity) (hω : ‖ω‖ = 1)
    (F : Velocity × Velocity → ℝ) :
    (∫ p, collisionKernel p.1 p.2 ω * F (scatterPair ω p)
      ∂((volume : Measure Velocity).prod volume)) =
      ∫ p, collisionKernel p.1 p.2 ω * F p
        ∂((volume : Measure Velocity).prod volume) := by
…

Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.collisionKernel, OAI.BoltzmannNonuniqueness.scatterPair

theorem OAI.BoltzmannNonuniqueness.scatter_relative_velocity line 117
Source documentation
The relative velocity is reflected in the plane normal to the collision normal.
```
theorem scatter_relative_velocity (v w ω : Velocity) :
    scatterLeft v w ω - scatterRight v w ω =
      (v - w) - (2 * normalComponent v w ω) • ω := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.scatterLeft, OAI.BoltzmannNonuniqueness.scatterRight, OAI.BoltzmannNonuniqueness.normalComponent
theorem OAI.BoltzmannNonuniqueness.scatter_relative_speed line 124
Source documentation
A unit-normal collision preserves the relative speed.
```
theorem scatter_relative_speed (v w ω : Velocity) (hω : ‖ω‖ = 1) :
    ‖scatterLeft v w ω - scatterRight v w ω‖ = ‖v - w‖ := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.scatterLeft, OAI.BoltzmannNonuniqueness.scatterRight
def OAI.BoltzmannNonuniqueness.collisionCutoff line 133
Source documentation
The common relative-speed cutoff used for both pre- and post-collisional variables.
```
def collisionCutoff (b : ℝ) : Set (Velocity × Velocity) := {p | ‖p.1 - p.2‖ < b}
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.collisionCutoff_preimage_scatterPair line 135

theorem OAI.BoltzmannNonuniqueness.collisionCutoff_indicator_scatterPair line 142

Source documentation

The cutoff indicator commutes with pre/post-collisional substitution.

theorem collisionCutoff_indicator_scatterPair (b : ℝ) (ω : Velocity) (hω : ‖ω‖ = 1)
    (F : Velocity × Velocity → ℝ) (p : Velocity × Velocity) :
    (collisionCutoff b).indicator F (scatterPair ω p) =
      (collisionCutoff b).indicator (fun q => F (scatterPair ω q)) p := by
…

Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.collisionCutoff, OAI.BoltzmannNonuniqueness.scatterPair

theorem OAI.BoltzmannNonuniqueness.scatterPair_cutoff_measurePreserving line 151
Source documentation
The collision map preserves Lebesgue measure restricted to the common cutoff.
```
theorem scatterPair_cutoff_measurePreserving (b : ℝ) (ω : Velocity) (hω : ‖ω‖ = 1) :
    MeasurePreserving (scatterPair ω)
      (((volume : Measure Velocity).prod volume).restrict (collisionCutoff b))
      (((volume : Measure Velocity).prod volume).restrict (collisionCutoff b)) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.scatterPair, OAI.BoltzmannNonuniqueness.collisionCutoff

theorem OAI.BoltzmannNonuniqueness.integral_cutoff_scatterPair line 160

Source documentation

Unweighted substitution on the exact strict relative-speed cutoff.

theorem integral_cutoff_scatterPair (b : ℝ) (ω : Velocity) (hω : ‖ω‖ = 1)
    (F : Velocity × Velocity → ℝ) :
    (∫ p in collisionCutoff b, F (scatterPair ω p)
      ∂((volume : Measure Velocity).prod volume)) =
      ∫ p in collisionCutoff b, F p ∂((volume : Measure Velocity).prod volume) :=
…

Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.collisionCutoff, OAI.BoltzmannNonuniqueness.scatterPair

theorem OAI.BoltzmannNonuniqueness.integral_cutoff_collisionKernel_scatterPair line 169

Source documentation

Kernel-weighted substitution on the manuscript's common collision cutoff.

theorem integral_cutoff_collisionKernel_scatterPair (b : ℝ) (ω : Velocity) (hω : ‖ω‖ = 1)
    (F : Velocity × Velocity → ℝ) :
    (∫ p in collisionCutoff b, collisionKernel p.1 p.2 ω * F (scatterPair ω p)
      ∂((volume : Measure Velocity).prod volume)) =
      ∫ p in collisionCutoff b, collisionKernel p.1 p.2 ω * F p
        ∂((volume : Measure Velocity).prod volume) := by
…

Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.collisionCutoff, OAI.BoltzmannNonuniqueness.collisionKernel, OAI.BoltzmannNonuniqueness.scatterPair

theorem OAI.BoltzmannNonuniqueness.normalComponent_neg_normal line 178
theorem OAI.BoltzmannNonuniqueness.scatterLeft_neg_normal line 183
Source documentation
Opposite normal representatives describe exactly the same scattering.
```
theorem scatterLeft_neg_normal (v w ω : Velocity) :
    scatterLeft v w (-ω) = scatterLeft v w ω := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.scatterLeft
theorem OAI.BoltzmannNonuniqueness.scatterRight_neg_normal line 187
theorem OAI.BoltzmannNonuniqueness.collisionKernel_neg_normal line 191
theorem OAI.BoltzmannNonuniqueness.scatterPair_neg_normal line 195
def OAI.BoltzmannNonuniqueness.CollisionCutoff.rate line 215
def OAI.BoltzmannNonuniqueness.CollisionCutoff.kernel line 217
def OAI.BoltzmannNonuniqueness.CollisionCutoff.frequency line 220
def OAI.BoltzmannNonuniqueness.CollisionCutoff.integrand line 223
def OAI.BoltzmannNonuniqueness.CollisionCutoff.gain line 226
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.kernel_scatter line 229
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.rate_nonneg line 234
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.rate_le line 238
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.measurable_rate line 244
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.integrable_frequency line 248
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.abs_frequency_le line 256
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.kernel_nonneg line 273
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.kernel_le line 279
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.integrand_le line 285
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.integrable_gain line 291
theorem OAI.BoltzmannNonuniqueness.CollisionCutoff.gain_le line 308
theorem OAI.BoltzmannNonuniqueness.CollisionNullSets.left_pair line 330
theorem OAI.BoltzmannNonuniqueness.CollisionNullSets.right_pair line 336
def OAI.BoltzmannNonuniqueness.CollisionNullSets.left line 342
def OAI.BoltzmannNonuniqueness.CollisionNullSets.right line 343
theorem OAI.BoltzmannNonuniqueness.CollisionNullSets.left_quasiMeasurePreserving line 345
theorem OAI.BoltzmannNonuniqueness.CollisionNullSets.right_quasiMeasurePreserving line 358
theorem OAI.BoltzmannNonuniqueness.CollisionNullSets.gain_congr line 371
theorem OAI.BoltzmannNonuniqueness.CollisionNullSets.cutoff_gain_congr line 384
theorem OAI.BoltzmannNonuniqueness.CollisionNullSets.frequency_congr line 397
theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.collision_fiber_test_fubini line 421