PlaneChart.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

The graph chart for a collision plane

The chart records actual three-dimensional velocities. Its displacement satisfies the collision-plane equation, and the three-dimensional ball restriction is precisely the transverse-plus-axial restriction used in the geometric slice estimate. Identifying its measure with the Carleman plane measure remains a separate change-of-variables theorem.

def OAI.BoltzmannNonuniqueness.PlaneChart.join line 25
theorem OAI.BoltzmannNonuniqueness.PlaneChart.transverse_join line 27
theorem OAI.BoltzmannNonuniqueness.PlaneChart.axial_join line 31
theorem OAI.BoltzmannNonuniqueness.PlaneChart.join_transverse_axial line 35
theorem OAI.BoltzmannNonuniqueness.PlaneChart.norm_join_sq line 39
theorem OAI.BoltzmannNonuniqueness.PlaneChart.transverse_sub line 42
theorem OAI.BoltzmannNonuniqueness.PlaneChart.axial_sub line 47
theorem OAI.BoltzmannNonuniqueness.PlaneChart.inner_split line 49
def OAI.BoltzmannNonuniqueness.PlaneChart.normal line 57
def OAI.BoltzmannNonuniqueness.PlaneChart.slope line 59
def OAI.BoltzmannNonuniqueness.PlaneChart.offset line 61
def OAI.BoltzmannNonuniqueness.PlaneChart.chart line 63
theorem OAI.BoltzmannNonuniqueness.PlaneChart.transverse_chart line 66
theorem OAI.BoltzmannNonuniqueness.PlaneChart.axial_chart line 71
theorem OAI.BoltzmannNonuniqueness.PlaneChart.chart_on_plane line 75
Source documentation
The graph chart lies on the collision plane whenever the transverse normal is nonzero.
```
theorem chart_on_plane (v p : Velocity) (z s : ℝ) (hn : normal v p ≠ 0) :
    inner ℝ (v - p) (chart v p z s - v) = 0 := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.PlaneChart.normal, OAI.BoltzmannNonuniqueness.PlaneChart.chart
theorem OAI.BoltzmannNonuniqueness.PlaneChart.chart_displacement_norm_sq line 94
Source documentation
Exact norm of the displacement, used for the genuine ball restriction.
```
theorem chart_displacement_norm_sq (v p : Velocity) (z s : ℝ) :
    ‖chart v p z s - v‖ ^ 2 =
      ‖line (direction (normal v p)) (offset v p - slope v p * z) s - transverse v‖ ^ 2 + z ^ 2 := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.PlaneChart.chart, OAI.BoltzmannNonuniqueness.PlaneChart.normal, OAI.BoltzmannNonuniqueness.PlaneChart.offset, OAI.BoltzmannNonuniqueness.PlaneChart.slope
theorem OAI.BoltzmannNonuniqueness.PlaneChart.chart_tangent_coordinate line 101
theorem OAI.BoltzmannNonuniqueness.PlaneChart.chart_injective line 106
Source documentation
The chart is one-to-one in its two free coordinates.
```
theorem chart_injective (v p : Velocity) (hn : normal v p ≠ 0) :
    Function.Injective (fun zs : ℝ × ℝ => chart v p zs.1 zs.2) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.PlaneChart.normal, OAI.BoltzmannNonuniqueness.PlaneChart.chart
theorem OAI.BoltzmannNonuniqueness.PlaneChart.chart_recovers line 117
Source documentation
Every velocity on the plane is recovered by its axial and tangent coordinates.
```
theorem chart_recovers (v p ξ : Velocity) (hn : normal v p ≠ 0)
    (hplane : inner ℝ (v - p) (ξ - v) = 0) :
    chart v p (axial ξ - axial v)
      (inner ℝ (quarterTurn (direction (normal v p))) (transverse ξ)) = ξ := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.PlaneChart.normal, OAI.BoltzmannNonuniqueness.PlaneChart.chart