From 50d4c51b231199109c557cb20b01441a3fbfe806 Mon Sep 17 00:00:00 2001 From: Joris van Winden Date: Fri, 31 Jul 2026 15:04:09 +0200 Subject: [PATCH 1/8] first version of viscous shock statement --- LeanEval/Analysis/PDE/ViscousShock.lean | 54 +++++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 LeanEval/Analysis/PDE/ViscousShock.lean diff --git a/LeanEval/Analysis/PDE/ViscousShock.lean b/LeanEval/Analysis/PDE/ViscousShock.lean new file mode 100644 index 000000000..4bc86447f --- /dev/null +++ b/LeanEval/Analysis/PDE/ViscousShock.lean @@ -0,0 +1,54 @@ +import Mathlib.Analysis.InnerProductSpace.Laplacian +import Mathlib.Topology.MetricSpace.Lipschitz +import Mathlib.Analysis.Normed.Operator.NormedSpace +import Mathlib.LinearAlgebra.Charpoly.Basic +import Mathlib.FieldTheory.Separable +import Mathlib.LinearAlgebra.Eigenspace.Basic +import Mathlib.Topology.EMetricSpace.BoundedVariation +import EvalTools.Markers + +namespace LeanEval +namespace Analysis +namespace PDE + +/-! +# Stability of viscous shock waves. + +This file proves the BV stability estimate for viscous shock waves. +-/ + +open Metric Filter Topology Set +open scoped NNReal Nat EReal ContDiff + +local notation:arg "ℝ^" n:arg => EuclideanSpace ℝ (Fin n) + +variable (n : ℕ) (A : ℝ^n → (ℝ^n →L[ℝ] ℝ^n)) (K : Set ℝ^n) + +/-- `A` is uniformly smoothly hyperbolic on a `K` if `A` is smooth, +and for every `x ∈ K` it holds that `A x` has `n` real distinct eigenvalues. -/ +structure IsHyperbolicOn: Prop where + smooth : ContDiff ℝ ∞ A + real_ev x (hx : x ∈ K) : (A x).charpoly.Splits + distinct_ev x (hx : x ∈ K) : (A x).charpoly.Separable + +/-- `u` is a global smooth solution if `u` is continuous for all `t` and `x`, smooth for +`t > 0` and solves the PDE in the classical sense for `t > 0`. -/ +structure IsSmoothGlobalSolution (u : ℝ → ℝ → (ℝ^n)) : Prop where + diff : ContDiffOn ℝ ∞ (Function.uncurry u) (Set.Ioi 0 ×ˢ Set.univ) + cont : ContinuousOn (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ) + pde : ∀ t > 0, ∀ x, (deriv (u · x) t) + A (u t x) (deriv (u t ·) x) = + iteratedDeriv 2 (u · x) t + +structure HasBVEstimateWith (δ C : EReal) : Prop where + estimate u (h_sol : IsSmoothGlobalSolution n A u) + (h_initial_bv : eVariationOn (u 0 ·) Set.univ ≤ δ) + (h_initial_lim : ∃ x ∈ K, Tendsto (u 0 ·) atBot (𝓝 x)) + t (ht : t > 0) : eVariationOn (u t ·) univ ≤ C * eVariationOn (u 0 ·) univ + +theorem a_priori_bv_estimate (hn : 1 ≤ n) (hK : IsCompact K) (h : IsSmoothHyperbolicOn n A K) : + ∃ δ > 0, ∃ C < ⊤, HasBVEstimateWith n A K δ C := + sorry + +end PDE +end Analysis +end LeanEval From 916a0989a067c002419b53138494deef853a4d9d Mon Sep 17 00:00:00 2001 From: Joris van Winden Date: Fri, 31 Jul 2026 15:34:46 +0200 Subject: [PATCH 2/8] clean up --- LeanEval/Analysis/PDE/ViscousShock.lean | 42 ++++++++++++++++--------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/LeanEval/Analysis/PDE/ViscousShock.lean b/LeanEval/Analysis/PDE/ViscousShock.lean index 4bc86447f..f8d77379d 100644 --- a/LeanEval/Analysis/PDE/ViscousShock.lean +++ b/LeanEval/Analysis/PDE/ViscousShock.lean @@ -12,21 +12,31 @@ namespace Analysis namespace PDE /-! -# Stability of viscous shock waves. +# Stability of small viscous shock waves. -This file proves the BV stability estimate for viscous shock waves. --/ +This file proves a stability estimate for solutions to the equation +$$u_t + A(u)u_x = u_xx$$, where $$A(u)$$ is an `n` by `n` strictly hyperbolic +matrix (i.e., it has `n` distinct real eigenvalues) which depends smoothly on $$u$$. + +The estimate, first proved in [1, Theorem 1.1], estimates the total variation of a solution at any time `t > 0` +in terms of the variation at the initial time (provided the initial variation is small). +Since the variation is invariant under spatial rescaling, the estimate is +uniform in the strength of the diffusion coefficient (which we take to be one for simplicity). +This allows to prove that vanishing viscosity approximations for hyperbolic conservation +laws converge to the entropy solutions. -open Metric Filter Topology Set +* [1]. Bianchini and Bressan, Vanishing viscosity solutions of nonlinear hyperbolic systems. Annals of Mathematics 161 (2005). +-/ +open Filter Topology Set Function open scoped NNReal Nat EReal ContDiff local notation:arg "ℝ^" n:arg => EuclideanSpace ℝ (Fin n) variable (n : ℕ) (A : ℝ^n → (ℝ^n →L[ℝ] ℝ^n)) (K : Set ℝ^n) -/-- `A` is uniformly smoothly hyperbolic on a `K` if `A` is smooth, +/-- `A` is (uniformly, smoothly) hyperbolic on `K` if `A` is smooth, and for every `x ∈ K` it holds that `A x` has `n` real distinct eigenvalues. -/ -structure IsHyperbolicOn: Prop where +structure IsHyperbolicOn : Prop where smooth : ContDiff ℝ ∞ A real_ev x (hx : x ∈ K) : (A x).charpoly.Splits distinct_ev x (hx : x ∈ K) : (A x).charpoly.Separable @@ -34,19 +44,23 @@ structure IsHyperbolicOn: Prop where /-- `u` is a global smooth solution if `u` is continuous for all `t` and `x`, smooth for `t > 0` and solves the PDE in the classical sense for `t > 0`. -/ structure IsSmoothGlobalSolution (u : ℝ → ℝ → (ℝ^n)) : Prop where - diff : ContDiffOn ℝ ∞ (Function.uncurry u) (Set.Ioi 0 ×ˢ Set.univ) - cont : ContinuousOn (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ) - pde : ∀ t > 0, ∀ x, (deriv (u · x) t) + A (u t x) (deriv (u t ·) x) = - iteratedDeriv 2 (u · x) t + diff : ContDiffOn ℝ ∞ (uncurry u) (Set.Ioi 0 ×ˢ Set.univ) + cont : ContinuousOn (uncurry u) (Set.Ici 0 ×ˢ Set.univ) + pde : ∀ t > 0, ∀ x, (deriv (u · x) t) + A (u t x) (deriv (u t ·) x) = iteratedDeriv 2 (u t ·) x -structure HasBVEstimateWith (δ C : EReal) : Prop where +/-- A total variation estimate holds if the total variation of any smooth solution +at time `t > 0` can be linearly estimated in terms of the total variation at time `0`, +provided the variation at time `0` is sufficiently small and the initial left limit of `u` +lies in `K` (see [1, Theorem 1]). +-/ +structure HasTVEstimateWith (δ C : EReal) : Prop where estimate u (h_sol : IsSmoothGlobalSolution n A u) - (h_initial_bv : eVariationOn (u 0 ·) Set.univ ≤ δ) + (h_initial_tv : eVariationOn (u 0 ·) univ ≤ δ) (h_initial_lim : ∃ x ∈ K, Tendsto (u 0 ·) atBot (𝓝 x)) t (ht : t > 0) : eVariationOn (u t ·) univ ≤ C * eVariationOn (u 0 ·) univ -theorem a_priori_bv_estimate (hn : 1 ≤ n) (hK : IsCompact K) (h : IsSmoothHyperbolicOn n A K) : - ∃ δ > 0, ∃ C < ⊤, HasBVEstimateWith n A K δ C := +theorem hyperbolic_tv_estimate (hn : 1 ≤ n) (hK : IsCompact K) (h : IsHyperbolicOn n A K) : + ∃ δ > 0, ∃ C < ⊤, HasTVEstimateWith n A K δ C := sorry end PDE From 308ba3151e9c4d249e83ca269277e596b871c699 Mon Sep 17 00:00:00 2001 From: Joris van Winden Date: Fri, 31 Jul 2026 15:53:13 +0200 Subject: [PATCH 3/8] tag as eval problem --- .../PDE/{ViscousShock.lean => HyperbolicViscosity.lean} | 1 + manifests/problems/hyperbolic_viscosity.toml | 8 ++++++++ 2 files changed, 9 insertions(+) rename LeanEval/Analysis/PDE/{ViscousShock.lean => HyperbolicViscosity.lean} (99%) create mode 100644 manifests/problems/hyperbolic_viscosity.toml diff --git a/LeanEval/Analysis/PDE/ViscousShock.lean b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean similarity index 99% rename from LeanEval/Analysis/PDE/ViscousShock.lean rename to LeanEval/Analysis/PDE/HyperbolicViscosity.lean index f8d77379d..b96467d7f 100644 --- a/LeanEval/Analysis/PDE/ViscousShock.lean +++ b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean @@ -59,6 +59,7 @@ structure HasTVEstimateWith (δ C : EReal) : Prop where (h_initial_lim : ∃ x ∈ K, Tendsto (u 0 ·) atBot (𝓝 x)) t (ht : t > 0) : eVariationOn (u t ·) univ ≤ C * eVariationOn (u 0 ·) univ +@[eval_problem] theorem hyperbolic_tv_estimate (hn : 1 ≤ n) (hK : IsCompact K) (h : IsHyperbolicOn n A K) : ∃ δ > 0, ∃ C < ⊤, HasTVEstimateWith n A K δ C := sorry diff --git a/manifests/problems/hyperbolic_viscosity.toml b/manifests/problems/hyperbolic_viscosity.toml new file mode 100644 index 000000000..b717b65b5 --- /dev/null +++ b/manifests/problems/hyperbolic_viscosity.toml @@ -0,0 +1,8 @@ +id = "hyperbolic_viscosity_tv" +title = "Total variation estimate for hyperbolic systems" +test = false +module = "LeanEval.Analysis.PDE.HyperbolicViscosity" +holes = ["hyperbolic_tv_estimate"] +submitter = "Joris van Winden" +source = "Bianchini and Bressan, Vanishing viscosity solutions of nonlinear hyperbolic systems. Annals of Mathematics 161 (2005)." +informal_solution = "Bianchini and Bressan, Vanishing viscosity solutions of nonlinear hyperbolic systems. Annals of Mathematics 161 (2005)." From e84e4f31a8160ab295fb818ea060552632a5cb82 Mon Sep 17 00:00:00 2001 From: Joris van Winden Date: Fri, 31 Jul 2026 16:12:07 +0200 Subject: [PATCH 4/8] change continuity to uniform continuity --- LeanEval/Analysis/PDE/HyperbolicViscosity.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean index b96467d7f..2b09cc091 100644 --- a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean +++ b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean @@ -1,10 +1,8 @@ import Mathlib.Analysis.InnerProductSpace.Laplacian -import Mathlib.Topology.MetricSpace.Lipschitz -import Mathlib.Analysis.Normed.Operator.NormedSpace -import Mathlib.LinearAlgebra.Charpoly.Basic import Mathlib.FieldTheory.Separable -import Mathlib.LinearAlgebra.Eigenspace.Basic +import Mathlib.LinearAlgebra.Charpoly.Basic import Mathlib.Topology.EMetricSpace.BoundedVariation +import Mathlib.Topology.MetricSpace.Lipschitz import EvalTools.Markers namespace LeanEval @@ -12,13 +10,13 @@ namespace Analysis namespace PDE /-! -# Stability of small viscous shock waves. +# Total variation stability of viscous hyperbolic systems This file proves a stability estimate for solutions to the equation $$u_t + A(u)u_x = u_xx$$, where $$A(u)$$ is an `n` by `n` strictly hyperbolic matrix (i.e., it has `n` distinct real eigenvalues) which depends smoothly on $$u$$. -The estimate, first proved in [1, Theorem 1.1], estimates the total variation of a solution at any time `t > 0` +The estimate, first proved in [1, Theorem 1], estimates the total variation of a solution at any time `t > 0` in terms of the variation at the initial time (provided the initial variation is small). Since the variation is invariant under spatial rescaling, the estimate is uniform in the strength of the diffusion coefficient (which we take to be one for simplicity). @@ -45,7 +43,7 @@ structure IsHyperbolicOn : Prop where `t > 0` and solves the PDE in the classical sense for `t > 0`. -/ structure IsSmoothGlobalSolution (u : ℝ → ℝ → (ℝ^n)) : Prop where diff : ContDiffOn ℝ ∞ (uncurry u) (Set.Ioi 0 ×ˢ Set.univ) - cont : ContinuousOn (uncurry u) (Set.Ici 0 ×ˢ Set.univ) + cont : ∀ t > 0, UniformContinuousOn (uncurry u) (Set.Icc 0 t ×ˢ Set.univ) pde : ∀ t > 0, ∀ x, (deriv (u · x) t) + A (u t x) (deriv (u t ·) x) = iteratedDeriv 2 (u t ·) x /-- A total variation estimate holds if the total variation of any smooth solution From 687b026abb23d3dd68dd58d2a61e7cdf0a372702 Mon Sep 17 00:00:00 2001 From: Joris van Winden Date: Mon, 3 Aug 2026 08:16:02 +0200 Subject: [PATCH 5/8] fix manifest --- LeanEval/Analysis/PDE/HyperbolicViscosity.lean | 2 +- manifests/problems/hyperbolic_viscosity.toml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean index 2b09cc091..a4e3c2e5c 100644 --- a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean +++ b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean @@ -58,7 +58,7 @@ structure HasTVEstimateWith (δ C : EReal) : Prop where t (ht : t > 0) : eVariationOn (u t ·) univ ≤ C * eVariationOn (u 0 ·) univ @[eval_problem] -theorem hyperbolic_tv_estimate (hn : 1 ≤ n) (hK : IsCompact K) (h : IsHyperbolicOn n A K) : +theorem hyperbolic_viscosity (hn : 1 ≤ n) (hK : IsCompact K) (h : IsHyperbolicOn n A K) : ∃ δ > 0, ∃ C < ⊤, HasTVEstimateWith n A K δ C := sorry diff --git a/manifests/problems/hyperbolic_viscosity.toml b/manifests/problems/hyperbolic_viscosity.toml index b717b65b5..77fddc1c7 100644 --- a/manifests/problems/hyperbolic_viscosity.toml +++ b/manifests/problems/hyperbolic_viscosity.toml @@ -1,8 +1,8 @@ -id = "hyperbolic_viscosity_tv" +id = "hyperbolic_viscosity" title = "Total variation estimate for hyperbolic systems" test = false module = "LeanEval.Analysis.PDE.HyperbolicViscosity" -holes = ["hyperbolic_tv_estimate"] +holes = ["hyperbolic_viscosity"] submitter = "Joris van Winden" source = "Bianchini and Bressan, Vanishing viscosity solutions of nonlinear hyperbolic systems. Annals of Mathematics 161 (2005)." informal_solution = "Bianchini and Bressan, Vanishing viscosity solutions of nonlinear hyperbolic systems. Annals of Mathematics 161 (2005)." From 2431bac743c5d4c174e6dd0a4e6dccf9727d549d Mon Sep 17 00:00:00 2001 From: Joris van Winden Date: Tue, 11 Aug 2026 16:02:17 +0200 Subject: [PATCH 6/8] add theorem docstring --- LeanEval/Analysis/PDE/HyperbolicViscosity.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean index a4e3c2e5c..79db54535 100644 --- a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean +++ b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean @@ -57,6 +57,7 @@ structure HasTVEstimateWith (δ C : EReal) : Prop where (h_initial_lim : ∃ x ∈ K, Tendsto (u 0 ·) atBot (𝓝 x)) t (ht : t > 0) : eVariationOn (u t ·) univ ≤ C * eVariationOn (u 0 ·) univ +/-- Total variation estimate for hyperbolic systems -/ @[eval_problem] theorem hyperbolic_viscosity (hn : 1 ≤ n) (hK : IsCompact K) (h : IsHyperbolicOn n A K) : ∃ δ > 0, ∃ C < ⊤, HasTVEstimateWith n A K δ C := From 34b6017734995be93b5fe37d60405be78efb71e6 Mon Sep 17 00:00:00 2001 From: Joris van Winden Date: Tue, 11 Aug 2026 16:07:45 +0200 Subject: [PATCH 7/8] change sorry to by sorry --- LeanEval/Analysis/PDE/HyperbolicViscosity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean index 79db54535..ba0a9a6dd 100644 --- a/LeanEval/Analysis/PDE/HyperbolicViscosity.lean +++ b/LeanEval/Analysis/PDE/HyperbolicViscosity.lean @@ -60,7 +60,7 @@ structure HasTVEstimateWith (δ C : EReal) : Prop where /-- Total variation estimate for hyperbolic systems -/ @[eval_problem] theorem hyperbolic_viscosity (hn : 1 ≤ n) (hK : IsCompact K) (h : IsHyperbolicOn n A K) : - ∃ δ > 0, ∃ C < ⊤, HasTVEstimateWith n A K δ C := + ∃ δ > 0, ∃ C < ⊤, HasTVEstimateWith n A K δ C := by sorry end PDE From f13b9f31122d6647c0a9bca868274671f3303190 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 21 Aug 2026 01:31:53 +0000 Subject: [PATCH 8/8] chore: add catalog lifecycle metadata to the manifest Main now requires `group`, `status`, `visible`, `statement_revision` and `tags` in every problem manifest (EvalTools/Markers.lean, added in 07848f4). Without them `validate-manifest` fails with "missing required key: group". Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011hxUxCg6joVz4hMa3m5Zh5 --- manifests/problems/hyperbolic_viscosity.toml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/manifests/problems/hyperbolic_viscosity.toml b/manifests/problems/hyperbolic_viscosity.toml index 77fddc1c7..9d6c4c9fa 100644 --- a/manifests/problems/hyperbolic_viscosity.toml +++ b/manifests/problems/hyperbolic_viscosity.toml @@ -1,5 +1,10 @@ id = "hyperbolic_viscosity" title = "Total variation estimate for hyperbolic systems" +group = "formalization-evaluation" +status = "draft" +visible = true +statement_revision = 1 +tags = [] test = false module = "LeanEval.Analysis.PDE.HyperbolicViscosity" holes = ["hyperbolic_viscosity"]