def TransportBurgers.SolvesTransport {n : ℕ} (X : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ) (u : (Fin (n + 1) → ℝ) → ℝ) : Prop

The transport equation $\sum_\mu X^\mu \partial_\mu u = 0$ associated to a vector field $X$ on $\mathbb{R}^{n+1}$. A function $u$ solves the transport equation at every point $p$ iff the directional derivative of $u$ along $X(p)$ vanishes.

def TransportBurgers.IsIntegralCurve {n : ℕ} (X : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ) (γ : ℝ → Fin (n + 1) → ℝ) : Prop

A curve $\gamma : \mathbb{R} \to \mathbb{R}^{n+1}$ is an integral curve of the vector field $X$ if $\gamma'(s) = X(\gamma(s))$ for all $s$.

theorem TransportBurgers.transport_constant_along_chars {n : ℕ} (X : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ) (u : (Fin (n + 1) → ℝ) → ℝ) (γ : ℝ → Fin (n + 1) → ℝ) (hu : SolvesTransport X u) (hγ : IsIntegralCurve X γ) (s : ℝ) (hu_diff : DifferentiableAt ℝ u (γ s)) (hγ_diff : DifferentiableAt ℝ γ s) : deriv (fun (s : ℝ) => u (γ s)) s = 0

Proposition 1.0.1 (Connection between transport equations and ODEs). If $u$ solves the transport equation $\sum_\mu X^\mu \partial_\mu u = 0$ and $\gamma$ is an integral curve of $X$, then $u$ is constant along $\gamma$, i.e. $\frac{d}{ds} u(\gamma(s)) = 0$.

def TransportBurgers.SolvesBurgers (u : ℝ → ℝ → ℝ) : Prop

Burger's equation $u_t + u\,u_x = 0$ in $1 + 1$ dimensions. A function $u(t, x)$ solves Burger's equation iff the time and space partial derivatives satisfy this nonlinear conservation law at every spacetime point.

theorem TransportBurgers.c1_implies_t_diff (u : ℝ → ℝ → ℝ) (hC1 : ContDiff ℝ 1 (Function.uncurry u)) (t x : ℝ) : DifferentiableAt ℝ (fun (t' : ℝ) => u t' x) t

Helper: if the uncurried form of $u : \mathbb{R} \to \mathbb{R} \to \mathbb{R}$ is $C^1$, then for fixed $x$ the slice $t' \mapsto u(t', x)$ is differentiable at $t$.

theorem TransportBurgers.c1_implies_x_diff (u : ℝ → ℝ → ℝ) (hC1 : ContDiff ℝ 1 (Function.uncurry u)) (t x : ℝ) : DifferentiableAt ℝ (fun (x' : ℝ) => u t x') x

Helper: if the uncurried form of $u$ is $C^1$, then for fixed $t$ the spatial slice $x' \mapsto u(t, x')$ is differentiable at $x$.

theorem TransportBurgers.c1_continuous_x (u : ℝ → ℝ → ℝ) (hC1 : ContDiff ℝ 1 (Function.uncurry u)) (t : ℝ) : Continuous fun (x : ℝ) => u t x

Helper: if $u$ is jointly $C^1$, then for fixed $t$ the spatial slice $x \mapsto u(t, x)$ is continuous.

theorem TransportBurgers.deriv_t_eq_fderiv_10 (u : ℝ → ℝ → ℝ) (hC1 : ContDiff ℝ 1 (Function.uncurry u)) (t x : ℝ) : deriv (fun (t' : ℝ) => u t' x) t = (fderiv ℝ (Function.uncurry u) (t, x)) (1, 0)

The partial time-derivative of $u$ equals the joint Fréchet derivative of the uncurried $u$ paired against the unit tangent vector $(1, 0)$.

theorem TransportBurgers.deriv_t_continuous_in_x (u : ℝ → ℝ → ℝ) (hC1 : ContDiff ℝ 1 (Function.uncurry u)) (t : ℝ) : Continuous fun (x : ℝ) => deriv (fun (t' : ℝ) => u t' x) t

For $u$ jointly $C^1$ and fixed $t$, the map $x \mapsto u_t(t, x)$ is continuous in the spatial variable.

theorem TransportBurgers.bounded_of_continuous_tendsto_zero (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_top : Filter.Tendsto f Filter.atTop (nhds 0)) (hf_bot : Filter.Tendsto f Filter.atBot (nhds 0)) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (x : ℝ), |f x| ≤ M

A continuous function $f : \mathbb{R} \to \mathbb{R}$ that decays to $0$ at both $\pm\infty$ is globally bounded: $\exists M \ge 0$ with $|f(x)| \le M$ for all $x$.

theorem TransportBurgers.c1_decay_implies_sq_integrable (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hf_top : Filter.Tendsto f Filter.atTop (nhds 0)) (hf_bot : Filter.Tendsto f Filter.atBot (nhds 0)) : MeasureTheory.Integrable (fun (x : ℝ) => f x ^ 2) MeasureTheory.volume

A continuous, integrable function on $\mathbb{R}$ that decays to $0$ at $\pm\infty$ has an integrable square: $f^2 \in L^1(\mathbb{R})$.

theorem TransportBurgers.c1_decay_implies_leibniz_hypotheses (u : ℝ → ℝ → ℝ) (T : ℝ) (_hC1 : ContDiff ℝ 1 (Function.uncurry u)) (_hdecay : ∀ t ∈ Set.Icc 0 T, Filter.Tendsto (fun (x : ℝ) => u t x) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (x : ℝ) => u t x) Filter.atBot (nhds 0)) (hInt_u : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ℝ) => u t x) MeasureTheory.volume) (hLeibnizBound : ∀ t' ∈ Set.Icc 0 T, ∃ (s : Set ℝ) (_ : s ∈ nhds t') (bound : ℝ → ℝ), (∀ᵐ (x : ℝ), ∀ t'' ∈ s, ‖deriv (fun (t''' : ℝ) => u t''' x ^ 2) t''‖ ≤ bound x) ∧ MeasureTheory.Integrable bound MeasureTheory.volume) (t' : ℝ) (_ht' : t' ∈ Set.Icc 0 T) : MeasureTheory.Integrable (fun (x : ℝ) => u t' x ^ 2) MeasureTheory.volume ∧ ∃ (s : Set ℝ) (_ : s ∈ nhds t'), (∀ᶠ (t'' : ℝ) in nhds t', MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => u t'' x ^ 2) MeasureTheory.volume) ∧ MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => deriv (fun (t'' : ℝ) => u t'' x ^ 2) t') MeasureTheory.volume ∧ ∃ (bound : ℝ → ℝ), (∀ᵐ (x : ℝ), ∀ t'' ∈ s, ‖deriv (fun (t''' : ℝ) => u t''' x ^ 2) t''‖ ≤ bound x) ∧ MeasureTheory.Integrable bound MeasureTheory.volume ∧ ∀ᵐ (x : ℝ), ∀ t'' ∈ s, HasDerivAt (fun (t''' : ℝ) => u t''' x ^ 2) (deriv (fun (t''' : ℝ) => u t''' x ^ 2) t'') t''

Packages the hypotheses needed to apply a Leibniz / differentiation-under-the-integral rule to $\int_{\mathbb{R}} u(t, x)^2 \, dx$: from $C^1$ regularity, spatial decay, spatial integrability, and a uniform local bound on $\partial_t (u^2)$, derive the exact ensemble of measurability, integrability, and pointwise differentiability hypotheses required.

theorem TransportBurgers.hasDerivAt_integral (f : ℝ → ℝ → ℝ) (t : ℝ) (hf_int : MeasureTheory.Integrable (f t) MeasureTheory.volume) {s : Set ℝ} (hs : s ∈ nhds t) (hf_meas : ∀ᶠ (t' : ℝ) in nhds t, MeasureTheory.AEStronglyMeasurable (f t') MeasureTheory.volume) (hf_deriv_meas : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => deriv (fun (t' : ℝ) => f t' x) t) MeasureTheory.volume) {bound : ℝ → ℝ} (h_bound : ∀ᵐ (x : ℝ), ∀ t' ∈ s, ‖deriv (fun (t'' : ℝ) => f t'' x) t'‖ ≤ bound x) (bound_int : MeasureTheory.Integrable bound MeasureTheory.volume) (h_diff_on : ∀ᵐ (x : ℝ), ∀ t' ∈ s, HasDerivAt (fun (t'' : ℝ) => f t'' x) (deriv (fun (t'' : ℝ) => f t'' x) t') t') : HasDerivAt (fun (t' : ℝ) => ∫ (x : ℝ), f t' x) (∫ (x : ℝ), deriv (fun (t' : ℝ) => f t' x) t) t

Differentiation under the integral sign (specialised wrapper): under the standard dominated-convergence hypotheses, the parameter integral $t \mapsto \int_{\mathbb{R}} f(t, x) \, dx$ has derivative $\int_{\mathbb{R}} \partial_t f(t, x) \, dx$ at $t$.

theorem TransportBurgers.l2_norm_conservation_burgers (u : ℝ → ℝ → ℝ) (hu : SolvesBurgers u) (T : ℝ) (_hT : T ≥ 0) (hC1 : ContDiff ℝ 1 (Function.uncurry u)) (hu_decay : ∀ t ∈ Set.Icc 0 T, Filter.Tendsto (fun (x : ℝ) => u t x) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (x : ℝ) => u t x) Filter.atBot (nhds 0)) (hInt_u : ∀ t ∈ Set.Icc 0 T, MeasureTheory.Integrable (fun (x : ℝ) => u t x) MeasureTheory.volume) (hLeibnizBound : ∀ t' ∈ Set.Icc 0 T, ∃ (s : Set ℝ) (_ : s ∈ nhds t') (bound : ℝ → ℝ), (∀ᵐ (x : ℝ), ∀ t'' ∈ s, ‖deriv (fun (t''' : ℝ) => u t''' x ^ 2) t''‖ ≤ bound x) ∧ MeasureTheory.Integrable bound MeasureTheory.volume) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ∫ (x : ℝ), u t x ^ 2 = ∫ (x : ℝ), u 0 x ^ 2

Proposition 2.0.1 (Burger's equation is a conservation law). Let $u(t, x)$ be a $C^1$ solution of Burger's equation on $[0, T] \times \mathbb{R}$ that decays to $0$ as $x \to \pm \infty$ uniformly for $t \in [0, T]$ (with suitable integrability of $u(t, \cdot)$ and a Leibniz-rule bound). Then the spatial $L^2$ norm is conserved: $$\int_{\mathbb{R}} u(t, x)^2 \, dx = \int_{\mathbb{R}} u(0, x)^2 \, dx \quad \text{for all } t \in [0, T].$$

structure TransportBurgers.Characteristics.BurgersCharacteristic (u : ℝ → ℝ → ℝ) (γ_t γ_x : ℝ → ℝ) : Prop

Definition 2.0.1 (Characteristic curves). A characteristic curve for Burger's equation with solution $u$ is a pair $(\gamma_t, \gamma_x) : \mathbb{R} \to \mathbb{R}^2$ satisfying the ODE system $$\frac{d}{ds} \gamma_t(s) = 1, \qquad \frac{d}{ds} \gamma_x(s) = u(\gamma_t(s), \gamma_x(s)).$$

• time_param (s : ℝ) : deriv γ_t s = 1
• space_param (s : ℝ) : deriv γ_x s = u (γ_t s) (γ_x s)

theorem TransportBurgers.Characteristics.burgers_chars_straight_lines (u : ℝ → ℝ → ℝ) (γ_t γ_x : ℝ → ℝ) (_hu : SolvesBurgers u) (hchar : BurgersCharacteristic u γ_t γ_x) (hconst : ∀ (s : ℝ), u (γ_t s) (γ_x s) = u (γ_t 0) (γ_x 0)) (_ht_init : γ_t 0 = 0) (hx_diff : Differentiable ℝ γ_x) (s : ℝ) : γ_x s = γ_x 0 + u (γ_t 0) (γ_x 0) * s

Proposition 2.0.3 (Burger characteristics are straight lines). Given a characteristic $(\gamma_t, \gamma_x)$ for Burger's equation along which $u$ is constant, the spatial component is a straight line: $\gamma_x(s) = \gamma_x(0) + u(\gamma_t(0), \gamma_x(0)) \cdot s$.

theorem TransportBurgers.Characteristics.burgers_char_zero_accel_time (u : ℝ → ℝ → ℝ) (γ_t γ_x : ℝ → ℝ) (hchar : BurgersCharacteristic u γ_t γ_x) (s : ℝ) : deriv (deriv γ_t) s = 0

The time component of a Burger's characteristic has zero acceleration: $\gamma_t''(s) = 0$ for all $s$ (a direct consequence of $\gamma_t'(s) = 1$).

theorem TransportBurgers.Characteristics.burgers_char_zero_accel_space (u : ℝ → ℝ → ℝ) (γ_t γ_x : ℝ → ℝ) (hchar : BurgersCharacteristic u γ_t γ_x) (hconst : ∀ (s : ℝ), deriv (fun (s : ℝ) => u (γ_t s) (γ_x s)) s = 0) (hx_diff : Differentiable ℝ γ_x) (s : ℝ) : deriv (deriv γ_x) s = 0

The spatial component of a Burger's characteristic has zero acceleration: if $u$ is constant along the characteristic, then $\gamma_x''(s) = 0$.