def TransportBurgers.IsBurgersCharacteristic (u : ℝ → ℝ → ℝ) (g0 g1 : ℝ → ℝ) : Prop

Predicate that a pair of curves $g_0, g_1 : \mathbb{R} \to \mathbb{R}$ forms a Burger's characteristic: $g_0'(s) = 1$ and $g_1'(s) = u(g_0(s), g_1(s))$.

structure TransportBurgers.IsCharacteristicCurve (u : ℝ → ℝ → ℝ) (γ : ℝ → ℝ × ℝ) : Prop

Bundled (paired) version of a Burger's characteristic curve $\gamma : \mathbb{R} \to \mathbb{R} \times \mathbb{R}$: the time component has derivative $1$ and the space component has derivative $u(\gamma_t, \gamma_x)$.

• time_param (s : ℝ) : HasDerivAt (fun (s : ℝ) => (γ s).1) 1 s
• spatial_eq (s : ℝ) : HasDerivAt (fun (s : ℝ) => (γ s).2) (u (γ s).1 (γ s).2) s

theorem TransportBurgers.burgers_char_zero_accel_time (g0 : ℝ → ℝ) (hg0 : ∀ (s : ℝ), deriv g0 s = 1) (s : ℝ) : deriv (deriv g0) s = 0

If $g_0' \equiv 1$ then $g_0$ has zero acceleration: $g_0''(s) = 0$ for all $s$. (Time-component analogue of straight-line characteristics.)

theorem TransportBurgers.burgers_char_zero_accel_space (u : ℝ → ℝ → ℝ) (g0 g1 : ℝ → ℝ) (hchar : IsBurgersCharacteristic u g0 g1) (hconst : ∀ (s : ℝ), deriv (fun (s : ℝ) => u (g0 s) (g1 s)) s = 0) (hg1_diff : Differentiable ℝ g1) (s : ℝ) : deriv (deriv g1) s = 0

Spatial-component analogue: if $u$ is constant along the characteristic $(g_0, g_1)$ then $g_1$ has zero acceleration, $g_1''(s) = 0$ for all $s$.

theorem TransportBurgers.ode_unique_zero_pos (w h : ℝ → ℝ) (hw_diff : Differentiable ℝ w) (hw0 : w 0 = 0) (hh_cont : Continuous h) (hw_eq : ∀ (s₀ : ℝ), HasDerivAt w (-w s₀ * h s₀) s₀) (s : ℝ) (hs : 0 ≤ s) : w s = 0

Uniqueness for the linear ODE $w'(s) = -w(s) \cdot h(s)$ with $w(0) = 0$ on the right half-line: any differentiable solution with continuous coefficient $h$ must vanish identically on $[0, \infty)$. Proved via Grönwall.

theorem TransportBurgers.ode_unique_zero (w h : ℝ → ℝ) (hw_diff : Differentiable ℝ w) (hw0 : w 0 = 0) (hh_cont : Continuous h) (hw_eq : ∀ (s₀ : ℝ), HasDerivAt w (-w s₀ * h s₀) s₀) (s : ℝ) : w s = 0

Two-sided uniqueness: any differentiable solution of $w'(s) = -w(s) h(s)$ with $w(0) = 0$ and continuous $h$ vanishes on all of $\mathbb{R}$.

theorem TransportBurgers.burgers_constant_along_straight_char (u : ℝ → ℝ → ℝ) (f : ℝ → ℝ) (hu : SolvesBurgers u) (hu_C1 : ContDiff ℝ 1 (Function.uncurry u)) (hdata : ∀ (x : ℝ), u 0 x = f x) (p s : ℝ) : u s (p + f p * s) = f p

Proposition 2.0.2 (Burger solutions are constant along characteristics). Let $u$ be a $C^1$ solution of Burger's equation with initial data $u(0, \cdot) = f$. Then along the straight characteristic emanating from $(0, p)$, the solution is constant: $u(s, p + f(p) \cdot s) = f(p)$ for all $s \in \mathbb{R}$.

theorem TransportBurgers.burgers_implicit_solution (u : ℝ → ℝ → ℝ) (f : ℝ → ℝ) (hu : SolvesBurgers u) (hu_C1 : ContDiff ℝ 1 (Function.uncurry u)) (hdata : ∀ (x : ℝ), u 0 x = f x) (t x p : ℝ) (hp : x = p + f p * t) : u t x = f p

Theorem 3.1 ("Solving" Burger's equation). Reformulation of burgers_constant_along_straight_char: if $(t, x)$ lies on the characteristic through $(0, p)$, i.e. $x = p + f(p) \cdot t$, then $u(t, x) = f(p)$.

theorem TransportBurgers.exists_gt_of_deriv_neg (f : ℝ → ℝ) (hf_diff : Differentiable ℝ f) (x₀ : ℝ) (hf'_neg : deriv f x₀ < 0) : ∃ x₁ > x₀, f x₁ < f x₀

If $f$ is differentiable and $f'(x_0) < 0$, then there exists some $x_1 > x_0$ with $f(x_1) < f(x_0)$. (A strict decrease just to the right of $x_0$.)

theorem TransportBurgers.singularity_forward_chars_cross (f : ℝ → ℝ) (hf_diff : Differentiable ℝ f) (x₀ : ℝ) (hf'_neg : deriv f x₀ < 0) : ∃ (p₀ : ℝ) (p₁ : ℝ) (t : ℝ), p₀ ≠ p₁ ∧ 0 < t ∧ p₀ + f p₀ * t = p₁ + f p₁ * t

If $f'(x_0) < 0$ for some $x_0$, then two characteristics for Burger's equation collide at some positive time: there exist distinct $p_0, p_1$ and $t > 0$ with $p_0 + f(p_0) t = p_1 + f(p_1) t$.

theorem TransportBurgers.singularity_forward_contradiction (u : ℝ → ℝ → ℝ) (f : ℝ → ℝ) (hdata : ∀ (x : ℝ), u 0 x = f x) (hconst_char : ∀ (p s : ℝ), u s (p + f p * s) = u 0 p) (hf_diff : Differentiable ℝ f) (x₀ : ℝ) (hf'_neg : deriv f x₀ < 0) : ∃ (p₀ : ℝ) (p₁ : ℝ) (t : ℝ) (x : ℝ), p₀ ≠ p₁ ∧ 0 < t ∧ f p₀ ≠ f p₁ ∧ u t x = f p₀ ∧ u t x = f p₁

The forward-time contradiction underlying the singularity theorem: if the initial data has $f'(x_0) < 0$, then there is a point $(t, x)$ with $t > 0$ where the constant-along-characteristics property forces $u(t, x) = f(p_0) = f(p_1)$ for distinct $p_0, p_1$ with $f(p_0) \ne f(p_1)$, a contradiction.

theorem TransportBurgers.implicit_function_theorem_bare (f : ℝ → ℝ) (hf_C1 : ContDiff ℝ 1 f) (hf'_nonneg : ∀ (x : ℝ), 0 ≤ deriv f x) : ∃ (p₀ : ℝ → ℝ → ℝ), (∀ (t x : ℝ), x = p₀ t x + f (p₀ t x) * t) ∧ (∀ (x : ℝ), p₀ 0 x = x) ∧ ContDiff ℝ 1 (Function.uncurry p₀)

Implicit Function Theorem (bare form). If $f \in C^1(\mathbb{R})$ with $f' \ge 0$ everywhere, then there exists a $C^1$ function $p_0(t, x)$ on $\mathbb{R}^2$ that inverts the characteristic relation $x = p + f(p) t$ and agrees with the identity at $t = 0$.

theorem TransportBurgers.transport_equation_from_ift (f : ℝ → ℝ) (hf_C1 : ContDiff ℝ 1 f) (hf'_nonneg : ∀ (x : ℝ), 0 ≤ deriv f x) (p₀ : ℝ → ℝ → ℝ) (hp₀_rel : ∀ (t x : ℝ), x = p₀ t x + f (p₀ t x) * t) (hp₀_C1 : ContDiff ℝ 1 (Function.uncurry p₀)) (t x : ℝ) : deriv (fun (t' : ℝ) => p₀ t' x) t + f (p₀ t x) * deriv (fun (x' : ℝ) => p₀ t x') x = 0

The characteristic inverse $p_0(t, x)$ satisfies the linear transport equation $\partial_t p_0 + f(p_0) \partial_x p_0 = 0$. Derived by implicit differentiation of the relation $x = p_0(t, x) + f(p_0(t, x)) t$.

theorem TransportBurgers.implicit_function_theorem_characteristic (f : ℝ → ℝ) (hf_C1 : ContDiff ℝ 1 f) (hf'_nonneg : ∀ (x : ℝ), 0 ≤ deriv f x) : ∃ (p₀ : ℝ → ℝ → ℝ), (∀ (t x : ℝ), x = p₀ t x + f (p₀ t x) * t) ∧ (∀ (x : ℝ), p₀ 0 x = x) ∧ ContDiff ℝ 1 (Function.uncurry p₀) ∧ ∀ (t x : ℝ), deriv (fun (t' : ℝ) => p₀ t' x) t + f (p₀ t x) * deriv (fun (x' : ℝ) => p₀ t x') x = 0

Combined IFT-with-transport statement: if $f \in C^1$ with $f' \ge 0$, then the characteristic inverse $p_0$ exists, is $C^1$, agrees with the identity at $t = 0$, satisfies $x = p_0 + f(p_0) t$, and obeys the transport PDE $\partial_t p_0 + f(p_0) \partial_x p_0 = 0$.

theorem TransportBurgers.burgers_C1_of_nonneg_deriv (f : ℝ → ℝ) (hf_C1 : ContDiff ℝ 1 f) (hf'_nonneg : ∀ (x : ℝ), 0 ≤ deriv f x) : ∃ (u : ℝ → ℝ → ℝ), SolvesBurgers u ∧ (∀ (x : ℝ), u 0 x = f x) ∧ ContDiff ℝ 1 (Function.uncurry u)

Existence direction of Theorem 4.1. If $f \in C^1(\mathbb{R})$ has $f'(x) \ge 0$ for all $x$, then Burger's equation admits a global $C^1$ solution $u(t, x) = f(p_0(t, x))$ with initial data $u(0, \cdot) = f$.

theorem TransportBurgers.burgers_singularity_C1_iff (f : ℝ → ℝ) (hf_C1 : ContDiff ℝ 1 f) : (∀ (x : ℝ), 0 ≤ deriv f x) ↔ ∃ (u : ℝ → ℝ → ℝ), SolvesBurgers u ∧ (∀ (x : ℝ), u 0 x = f x) ∧ ContDiff ℝ 1 (Function.uncurry u)

Theorem 4.1 (Sharp Characterization of Singularity Formation in Burger's Equation). For initial data $f \in C^1(\mathbb{R})$, Burger's equation $u_t + u u_x = 0$ has a global $C^1$ solution on $[0, \infty) \times \mathbb{R}$ with $u(0, \cdot) = f$ if and only if $f'(x) \ge 0$ for all $x \in \mathbb{R}$. Equivalently, singularities form in finite time iff the initial data has a strictly decreasing portion.