CarlemanNormalCoordinates.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Energy algebra on a Carleman collision plane

These are the exact geometric and Gaussian identities used in Section 3. The coarea/disintegration formula expressing the gain as a plane integral is a separate theorem and is not assumed or asserted here.

def OAI.BoltzmannNonuniqueness.companionVelocity line 23
Source documentation
The unobserved outgoing velocity is fixed by momentum conservation.
```
def companionVelocity (p ξ v : Velocity) : Velocity := p + ξ - v
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.carleman_energy line 26
Source documentation
The plane equation in the Carleman representation is exactly the energy equation.
```
theorem carleman_energy (p ξ v : Velocity)
    (h : inner ℝ (v - p) (ξ - v) = 0) :
    ‖p‖ ^ 2 + ‖ξ‖ ^ 2 = ‖v‖ ^ 2 + ‖companionVelocity p ξ v‖ ^ 2 := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.companionVelocity
theorem OAI.BoltzmannNonuniqueness.carleman_observed_energy_le line 36
Source documentation
The observed speed is bounded by the total incoming energy.
```
theorem carleman_observed_energy_le (p ξ v : Velocity)
    (h : inner ℝ (v - p) (ξ - v) = 0) :
    ‖v‖ ^ 2 ≤ ‖p‖ ^ 2 + ‖ξ‖ ^ 2 := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.carleman_bracket_sq_le line 43
Source documentation
Squared Japanese-bracket inequality used to transfer the polynomial weight.
```
theorem carleman_bracket_sq_le (p ξ v : Velocity)
    (h : inner ℝ (v - p) (ξ - v) = 0) :
    1 + ‖v‖ ^ 2 ≤ (1 + ‖p‖ ^ 2) * (1 + ‖ξ‖ ^ 2) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
theorem OAI.BoltzmannNonuniqueness.carleman_bracket_le line 49
theorem OAI.BoltzmannNonuniqueness.carleman_gaussian_ratio line 57
Source documentation
The Gaussian ratio identity in equation ker:energy-factor.
```
theorem carleman_gaussian_ratio (p ξ v : Velocity)
    (h : inner ℝ (v - p) (ξ - v) = 0) :
    Real.exp (-‖ξ‖ ^ 2) / Real.exp (-‖v‖ ^ 2) =
      Real.exp (‖p‖ ^ 2 - ‖companionVelocity p ξ v‖ ^ 2) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.companionVelocity
abbrev OAI.BoltzmannNonuniqueness.CarlemanCoordinates.V line 80
def OAI.BoltzmannNonuniqueness.CarlemanCoordinates.frameMatrix line 82
def OAI.BoltzmannNonuniqueness.CarlemanCoordinates.frame line 87
theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.frame_apply line 89
theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.frameMatrix_det line 95
theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.frame_dot line 102
theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.frame_map_volume line 110
theorem OAI.BoltzmannNonuniqueness.CarlemanCoordinates.unit_frame_map_volume line 119