def Burger.IsBurgerSolution (u : ℝ → ℝ → ℝ) : Prop

A function $u(t, x)$ is a (classical) solution of Burger's equation $\partial_t u + u\,\partial_x u = 0$ if it is $C^1$ and satisfies the PDE pointwise.

def Burger.IsCharacteristicCurve (u : ℝ → ℝ → ℝ) (γ₀ γ₁ : ℝ → ℝ) : Prop

A pair $(\gamma_0, \gamma_1)$ is a characteristic curve of Burger's equation if $\frac{d}{ds}\gamma_0 = 1$ and $\frac{d}{ds}\gamma_1 = u(\gamma_0(s), \gamma_1(s))$ (Definition 2.0.1).

theorem Burger.differentiable_along_char (u : ℝ → ℝ → ℝ) (γ₀ γ₁ : ℝ → ℝ) (hC1 : ContDiff ℝ 1 (Function.uncurry u)) (hγ₀_diff : Differentiable ℝ γ₀) (hγ₁_diff : Differentiable ℝ γ₁) : Differentiable ℝ fun (s : ℝ) => u (γ₀ s) (γ₁ s)

Helper: if $u$ is $C^1$ and $\gamma_0, \gamma_1$ are differentiable, then $s \mapsto u(\gamma_0(s), \gamma_1(s))$ is differentiable.

theorem Burger.deriv_along_char_eq_zero (u : ℝ → ℝ → ℝ) (γ₀ γ₁ : ℝ → ℝ) (hu : IsBurgerSolution u) (hchar : IsCharacteristicCurve u γ₀ γ₁) (hγ₀_diff : Differentiable ℝ γ₀) (hγ₁_diff : Differentiable ℝ γ₁) (s : ℝ) : deriv (fun (s : ℝ) => u (γ₀ s) (γ₁ s)) s = 0

If $u$ is a $C^1$ solution to Burger's equation and $(\gamma_0, \gamma_1)$ is a characteristic curve, then $\frac{d}{ds} u(\gamma_0(s), \gamma_1(s)) = 0$.

theorem Burger.burger_constant_along_characteristics (u : ℝ → ℝ → ℝ) (γ₀ γ₁ : ℝ → ℝ) (hu : IsBurgerSolution u) (hchar : IsCharacteristicCurve u γ₀ γ₁) (hγ₀_diff : Differentiable ℝ γ₀) (hγ₁_diff : Differentiable ℝ γ₁) (s₁ s₂ : ℝ) : u (γ₀ s₁) (γ₁ s₁) = u (γ₀ s₂) (γ₁ s₂)

Proposition 2.0.2: $C^1$ solutions to Burger's equation are constant along characteristic curves.