feat(Navier-Stokes): formalization of Navier–Stokes existence and smoothness

[lecopivo]

Formalization of Navier-Stokes existence and smoothness problem as described in https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf

Potentially issues:

• not immediately obvious that fderiv ℝ (v · t) x (v x t) is the convective term and that div is divergence
• the growth conditions uses ‖iteratedFDeriv ℝ n v₀ x‖ instead of |∂^α u(x,t)| but it should be equivalent
• at various places I'm not completely sure if there should be t ≥ 0 or t > 0 as fderiv might not give what we think at t=0. Mainly in NavierStokesExistenceAndSmoothness.navierStokes

Note:

• I didn't use the unicode character nu for viscosity as it looks too similar to the letter v which is used for velocity.
• bikeshead: should it use v(x,t)(aligned with the official statement) or v(t,x) that is more mathlib aligned?
• should it be formulated in an arbitrary dimension and then instantiated for n:=3?

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[YaelDillies]

Could you add way more documentation? I would make sure we're at least at mathlib standard (every def has a docstring), and hopefully go even further by writing down explicitly all the design decisions you've taken.

I didn't use the unicode character nu for viscosity as it looks too similar to the letter v which is used for velocity.

This seems fine.

bikeshead: should it use v(x,t) (aligned with the official statement) or v(t,x) that is more mathlib aligned?

I don't mind, so long as the discrepancy is clearly documented.

should it be formulated in an arbitrary dimension and then instantiated for n:=3?

Sure! That seems very reasonable so long as it isn't too difficult to do so. I assume it's already solved for n = 2? If so, it seems reasonable to have one statement for n = 2, one for n = 3 and one for all n, the first one being solved and the other two open.

[lecopivo]

@YaelDillies Hopefully, I have addressed all the issues.

The docs strings are mostly AI generated but they sound good to me and I don't really know what else I would write there.

[YaelDillies]

Suggested change

	(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :
	∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ (f:=0) v p := sorry
	(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :
	∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ (f:=0) v p := sorry

Same below

[YaelDillies]

Suggested change

	/--
	/--

[YaelDillies]

What about

Suggested change

	structure InitialVelocityConditionRn {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop
	structure InitialVelocityConditionDecay {n : ℕ} (v₀ : ℝ^n → ℝ^n) : Prop

instead? In both cases, the function has domain R^n, so Rn is a bit confusing as a way to distinguish

[YaelDillies]

The source uses

Suggested change

	(v₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn v₀) :
	(u₀ : ℝ³ → ℝ³) (hv₀ : InitialVelocityConditionRn u₀) :

instead. Maybe you could do that so that nu can become \nu?

[YaelDillies]

Technically, the periodicity of pressure isn't stated anywhere. Could you leave a comment to that effect?

[mirefek]

Errata on page 6 says also $p$ should be periodic.

[YaelDillies]

Condition 1 is also stated for t = 0. Could you explain the discrepancy in a comment?

[YaelDillies]

Suggested change

	/-- The velocity is square-integrable at each time t ≥ 0. -/
	/-- The velocity is square-integrable at each time t ≥ 0 (condition 7). -/

[YaelDillies]

Suggested change

	∃ (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
	InitialVelocityConditionRn v₀ ∧ ForceConditionRn f ∧
	¬(∃ v p, NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ f v p) := sorry
	∃ (v₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
	InitialVelocityConditionRn v₀ ∧ ForceConditionRn f ∧
	\forall v p, ¬ NavierStokesExistenceAndSmoothnessRn (n:=3) nu v₀ f v p := sorry

maybe?

[mirefek]

We looked at it with Tomáš Bárta (teacher of ODE at Charles University), and it looks good to us.

[mirefek]

More from Tomáš Bárta:

the formulation of NS seems correct to me but I have some remarks:

1. Should there be 'for all nu>0' in all theorems?

It seems strange that there is 'for all nu' in parts A, B (existence of global smooth solutions) and also 'for all nu' in parts C, D (non-existence of globally defined smooth solutions). In fact, if non-existence is proved for one nu, by a rescaling procedure it is proved for all positive nu (with another v_0 and f). So, it does not matter whether there is 'for all nu' or 'there exists nu'. But may be it would be better to write 'there exists nu>0' in parts C, D? I suggest to ask an NS expert concerning this.

2. Problems with $t>0$ and $t\ge 0$.

The present lean formulation writes $t>0$ in some conditions instead of $t\ge 0$ and the reason seems to be the language. Why don't you use iteratedFDerivWithin instead of iteratedFDeriv. Wouldn't it allow to work on $t\ge 0$? Maybe this would be a more elegant solution. (iteratedFDerivWithin seems to be used in definition of ContDiffOn, so we need it anyway)