AxialFlow.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

The monotone implicit axial flow

The cold jet profile in Section 4 of the supplied manuscript is σ + α * tanh (γ * z / s). Its characteristic map is expanding, giving a unique implicit velocity at every nonnegative time. The proof uses continuity, the intermediate value theorem, and monotonicity. No differentiability or unproved kinetic estimate is assumed.

def OAI.BoltzmannNonuniqueness.AxialFlow.profile line 33
Source documentation
The initial axial velocity at scale s.
```
def profile (σ α γ s z : ℝ) : ℝ := σ + α * Real.tanh (γ * z / s)
```
def OAI.BoltzmannNonuniqueness.AxialFlow.characteristic line 36
Source documentation
The spatial position at time t of a characteristic starting from z.
```
def characteristic (σ α γ s t z : ℝ) : ℝ := z + t * profile σ α γ s z
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.profile
def OAI.BoltzmannNonuniqueness.AxialFlow.residual line 39
Source documentation
The residual of the implicit velocity equation at the proposed velocity u.
```
def residual (σ α γ s t z u : ℝ) : ℝ :=
…
```
theorem OAI.BoltzmannNonuniqueness.AxialFlow.tanh_monotone line 42
theorem OAI.BoltzmannNonuniqueness.AxialFlow.tanh_continuous line 49
theorem OAI.BoltzmannNonuniqueness.AxialFlow.continuous_profile line 54
theorem OAI.BoltzmannNonuniqueness.AxialFlow.profile_monotone line 59
theorem OAI.BoltzmannNonuniqueness.AxialFlow.profile_sub_center_le line 66
theorem OAI.BoltzmannNonuniqueness.AxialFlow.continuous_residual line 72

theorem OAI.BoltzmannNonuniqueness.AxialFlow.characteristic_sub_ge line 78

Source documentation

The characteristic map expands ordered distances by at least one.

theorem characteristic_sub_ge {σ α γ s t x y : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht : 0 ≤ t) (hxy : x ≤ y) :
    y - x ≤ characteristic σ α γ s t y - characteristic σ α γ s t x := by
…

Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.characteristic

theorem OAI.BoltzmannNonuniqueness.AxialFlow.characteristic_strictMono line 86
theorem OAI.BoltzmannNonuniqueness.AxialFlow.residual_sub_ge line 94
Source documentation
The scalar residual expands ordered velocity differences by at least one.
```
theorem residual_sub_ge {σ α γ s t z u v : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht : 0 ≤ t) (huv : u ≤ v) :
    v - u ≤ residual σ α γ s t z v - residual σ α γ s t z u := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.residual
theorem OAI.BoltzmannNonuniqueness.AxialFlow.residual_strictMono line 102
theorem OAI.BoltzmannNonuniqueness.AxialFlow.exists_residual_zero line 111
Source documentation
The implicit equation has a root between the two extremal axial speeds, even without a sign restriction on time. Nonnegative time will be used for uniqueness.
```
theorem exists_residual_zero {σ α γ s t z : ℝ} (hα : 0 ≤ α) :
    ∃ u ∈ Icc (σ - α) (σ + α), residual σ α γ s t z u = 0 := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.residual
theorem OAI.BoltzmannNonuniqueness.AxialFlow.existsUnique_implicit_velocity line 126
def OAI.BoltzmannNonuniqueness.AxialFlow.velocity line 138
Source documentation
The implicit velocity selected by the inverse of the residual. Its defining equation and uniqueness are proved below under the physical parameter restrictions.
```
def velocity (σ α γ s t z : ℝ) : ℝ := invFun (residual σ α γ s t z) 0
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.residual
theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_spec line 140
theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_unique line 146
theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_sub_center_le line 152
theorem OAI.BoltzmannNonuniqueness.AxialFlow.characteristic_inverse_lipschitz line 158
Source documentation
The inverse characteristic map is 1-Lipschitz in the spatial coordinate.
```
theorem characteristic_inverse_lipschitz {σ α γ s t x y : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht : 0 ≤ t) :
    |x - y| ≤ |characteristic σ α γ s t x - characteristic σ α γ s t y| := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.characteristic
theorem OAI.BoltzmannNonuniqueness.AxialFlow.residual_inverse_lipschitz line 172
Source documentation
The inverse residual is 1-Lipschitz; this estimate does not require differentiation.
```
theorem residual_inverse_lipschitz {σ α γ s t z u v : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht : 0 ≤ t) :
    |u - v| ≤ |residual σ α γ s t z u - residual σ α γ s t z v| := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.residual
theorem OAI.BoltzmannNonuniqueness.AxialFlow.thermal_velocity_error line 187
Source documentation
A thermal perturbation of the implicit equation perturbs the velocity by at most its amplitude. This is the compressed axial velocity estimate used for cold cores.
```
theorem thermal_velocity_error {σ α γ s t z p δ : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht : 0 ≤ t)
    (hp : p = profile σ α γ s (z - t * p) + δ) :
    |p - velocity σ α γ s t z| ≤ |δ| := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.profile, OAI.BoltzmannNonuniqueness.AxialFlow.velocity
def OAI.BoltzmannNonuniqueness.AxialFlow.foot line 202
Source documentation
The initial spatial coordinate of the characteristic passing through (t,z).
```
def foot (σ α γ s t z : ℝ) : ℝ := z - t * velocity σ α γ s t z
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.velocity
theorem OAI.BoltzmannNonuniqueness.AxialFlow.characteristic_foot line 204
theorem OAI.BoltzmannNonuniqueness.AxialFlow.foot_characteristic line 211
theorem OAI.BoltzmannNonuniqueness.AxialFlow.characteristic_bijective line 217
theorem OAI.BoltzmannNonuniqueness.AxialFlow.foot_lipschitz line 225
Source documentation
Spatial separation does not increase when characteristics are traced backwards.
```
theorem foot_lipschitz {σ α γ s t z w : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht : 0 ≤ t) :
    |foot σ α γ s t z - foot σ α γ s t w| ≤ |z - w| := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.foot
theorem OAI.BoltzmannNonuniqueness.AxialFlow.foot_lipschitzWith line 232
theorem OAI.BoltzmannNonuniqueness.AxialFlow.continuous_velocity line 240
theorem OAI.BoltzmannNonuniqueness.AxialFlow.free_flight_foot_error line 250
Source documentation
A particle launched with thermal velocity error δ stays within t * |δ| in the inverse spatial coordinate. This is the axial-distance estimate in the transported cold-core barrier.
```
theorem free_flight_foot_error {σ α γ s t z δ : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht : 0 ≤ t) :
    |foot σ α γ s t (z + t * (profile σ α γ s z + δ)) - z| ≤ t * |δ| := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.foot, OAI.BoltzmannNonuniqueness.AxialFlow.profile
theorem OAI.BoltzmannNonuniqueness.AxialFlow.foot_monotone line 262
theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_monotone line 269
theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_on_characteristic line 281
Source documentation
The implicit velocity is constant on its own characteristic, including when it is traced backwards to an earlier nonnegative time.
```
theorem velocity_on_characteristic {σ α γ s t₁ t₂ z : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht₂ : 0 ≤ t₂) :
    velocity σ α γ s t₂
      (z - (t₁ - t₂) * velocity σ α γ s t₁ z) = velocity σ α γ s t₁ z := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.velocity
theorem OAI.BoltzmannNonuniqueness.AxialFlow.characteristic_matching line 294
Source documentation
Characteristic matching, the inequality in Section 8: tracing with an arbitrary speed cannot reduce its discrepancy from the earlier cold-flow velocity.
```
theorem characteristic_matching {σ α γ s t₁ t₂ z w : ℝ}
    (hα : 0 ≤ α) (hγ : 0 ≤ γ) (hs : 0 < s) (ht₂ : 0 ≤ t₂) (ht : t₂ ≤ t₁) :
    |w - velocity σ α γ s t₁ z| ≤
      |w - velocity σ α γ s t₂ (z - (t₁ - t₂) * w)| := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialFlow.velocity

theorem OAI.BoltzmannNonuniqueness.AxialFlow.density_coefficient_le_of_constant line 319

Source documentation

An algebraic form of the density-coefficient estimate. The two conditions on C absorb the spatial scale and the compressed-time scale separately.

theorem density_coefficient_le_of_constant {K S s t k C : ℝ}
    (hK : 0 ≤ K) (hS : 0 ≤ S) (hS1 : S ≤ 1) (hs : 0 < s) (ht : 0 ≤ t)
    (hk : 0 < k) (hC : 1 ≤ C) (hCk : 1 ≤ C * k) :
    K * S / (s + t * k * S) ≤ K * C / (s + t) := by
…

theorem OAI.BoltzmannNonuniqueness.AxialFlow.density_coefficient_le line 341
Source documentation
Uniform density coefficient bound for the cold-core Jacobian. In the manuscript k is α * γ and S is a squared hyperbolic secant.
```
theorem density_coefficient_le {K S s t k : ℝ}
    (hK : 0 ≤ K) (hS : 0 ≤ S) (hS1 : S ≤ 1) (hs : 0 < s) (ht : 0 ≤ t)
    (hk : 0 < k) :
    K * S / (s + t * k * S) ≤ K * max 1 (1 / k) / (s + t) := by
…
```
def OAI.BoltzmannNonuniqueness.AxialSlices.lineProfile line 372
def OAI.BoltzmannNonuniqueness.AxialSlices.lineConstant line 374
theorem OAI.BoltzmannNonuniqueness.AxialSlices.lineProfile_pos line 376
theorem OAI.BoltzmannNonuniqueness.AxialSlices.integrable_lineProfile line 380
theorem OAI.BoltzmannNonuniqueness.AxialSlices.lineConstant_pos line 386
theorem OAI.BoltzmannNonuniqueness.AxialSlices.lineProfile_scale line 396
theorem OAI.BoltzmannNonuniqueness.AxialSlices.integrable_singular_line line 410
theorem OAI.BoltzmannNonuniqueness.AxialSlices.singular_line_formula line 419
Source documentation
Exact singular line integral, including finiteness in a separate theorem above.
```
theorem singular_line_formula {q A : ℝ} (hq : 1 < q) (hA : A ≠ 0) :
    Integrable (fun s : ℝ => (A ^ 2 + s ^ 2) ^ (-q / 2)) ∧
      (∫ s : ℝ, (A ^ 2 + s ^ 2) ^ (-q / 2)) = lineConstant q * |A| ^ (1 - q) := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.AxialSlices.lineConstant
def OAI.BoltzmannNonuniqueness.AxialFlow.interiorArgumentBound line 456
theorem OAI.BoltzmannNonuniqueness.AxialFlow.interiorArgumentBound_nonneg line 459
theorem OAI.BoltzmannNonuniqueness.AxialFlow.abs_argument_le_of_tanh line 462
theorem OAI.BoltzmannNonuniqueness.AxialFlow.velocity_interior_small_scale line 475