structure BurgersCharacteristicCurves (u : ℝ → ℝ → ℝ) (γ_t γ_x : ℝ → ℝ) : Prop

The defining ODE system for a characteristic curve $(\gamma_t, \gamma_x)$ of Burger's equation $\partial_t u + u\,\partial_x u = 0$ (Definition 2.0.1): $\tfrac{d}{ds}\gamma_t = 1$ and $\tfrac{d}{ds}\gamma_x = u(\gamma_t(s), \gamma_x(s))$.

• time_deriv (s : ℝ) : HasDerivAt γ_t 1 s
• space_deriv (s : ℝ) : HasDerivAt γ_x (u (γ_t s) (γ_x s)) s

structure BurgersCharacteristicPaired (u : ℝ → ℝ → ℝ) (γ : ℝ → ℝ × ℝ) : Prop

Same as BurgersCharacteristicCurves, but packaged with a single curve $\gamma : \mathbb{R} \to \mathbb{R} \times \mathbb{R}$ whose two components play the role of $\gamma_t$ and $\gamma_x$.

• time_deriv (s : ℝ) : HasDerivAt (fun (s : ℝ) => (γ s).1) 1 s
• space_deriv (s : ℝ) : HasDerivAt (fun (s : ℝ) => (γ s).2) (u (γ s).1 (γ s).2) s