`BookProof.NavierStokesFlow.nsFlow_unique_solution` (psi : Fin n → ℂ) (y : ℝ → Fin n → ℂ) (hy : ∀ t, HasDerivAt y ((Complex.I • nsHamiltonian d) *ᵥ y t) t) (hy0 : y 0 = psi) (t : ℝ

Proved

BookProof.NavierStokesFlow.nsFlow_unique_solution

by leonardopedro · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesCauchy.

BookProof.NavierStokesFlow.nsFlow_unique_solution (psi : Fin n → ℂ) (y : ℝ → Fin n → ℂ) (hy : ∀ t, HasDerivAt y ((Complex.I • nsHamiltonian d) *ᵥ y t) t) (hy0 : y 0 = psi) (t : ℝ) : y t = nsFlowUnitary d t *ᵥ psi

Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.nsFlow_unique_solution.

Preamble

-- Generated from ChapterNavierStokesCauchy.lean — theorem BookProof.NavierStokesFlow.nsFlow_unique_solution
import Mathlib
import Definitions.Def_ChapterNavierStokesCauchy
import Definitions.Def_ChapterNavierStokesFlow
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow


open scoped BigOperators Matrix Matrix.Norms.Operator

variable {n : ℕ}
variable {n : ℕ} (d : NSTruncation n)

Formal statement

theorem BookProof.NavierStokesFlow.nsFlow_unique_solution (psi : Fin n → ℂ) (y : ℝ → Fin n → ℂ)
    (hy : ∀ t, HasDerivAt y ((Complex.I • nsHamiltonian d) *ᵥ y t) t) (hy0 : y 0 = psi)
    (t : ℝ) : y t = nsFlowUnitary d t *ᵥ psi := by sorry

View graph