`BookProof.NavierStokesFlow.nsCauchy_existsUnique` (psi : Fin n → ℂ) : ∃! y : ℝ → Fin n → ℂ, y 0 = psi ∧ ∀ t, HasDerivAt y ((Complex.I • nsHamiltonian d) *ᵥ y t) t

Initializing...

`BookProof.NavierStokesFlow.nsCauchy_existsUnique` (psi : Fin n → ℂ) : ∃! y : ℝ → Fin n → ℂ, y 0 = psi ∧ ∀ t, HasDerivAt y ((Complex.I • nsHamiltonian d) *ᵥ y t) t · Prove2Me