def NavierStokesEq.lerayProjector (k : Index3) (w : Fin 3 → ℂ) : Fin 3 → ℂ

Le Projecteur de Leray en Fourier. P_k(w) = w - k (k · w) / |k|²

Equations

• One or more equations did not get rendered due to their size.

def NavierStokesEq.triadicSummand (u_hat v_hat : Index3 → Fin 3 → ℂ) (k p : Index3) : Fin 3 → ℂ

Le terme intérieur de la convolution triadique pour le vecteur d'onde k.

Equations

• NavierStokesEq.triadicSummand u_hat v_hat k p = fun (i : Fin 3) => (Complex.I * ∑ i : Fin 3, u_hat p i * ↑((k - p) i)) * v_hat (k - p) i

def NavierStokesEq.convectionOperator (u v : Index3 → Fin 3 → ℂ) (k : Index3) : Fin 3 → ℂ

L'Opérateur Bilinéaire de Convection B(u,v) = P(u · ∇ v) évalué au mode de Fourier k.

Equations

• NavierStokesEq.convectionOperator u v k = NavierStokesEq.lerayProjector k (∑' (p : Index3), NavierStokesEq.triadicSummand u v k p)

structure NavierStokesEq.NavierStokesFlow : Type

La définition dynamique absolue d'un fluide de Navier-Stokes.

• u : ℝ → Index3 → Fin 3 → ℂ
• nu : ℝ
• nu_pos : self.nu > 0
• evolution (t : ℝ) (k : Index3) : let k_sq := ∑ i : Fin 3, ↑↑(k i) ^ 2; let u_k := fun (s : ℝ) => self.u s k; let dissipation := -(↑self.nu * k_sq) • u_k t; let convection := convectionOperator (self.u t) (self.u t) k; HasDerivAt u_k (dissipation - convection) t

def NavierStokesEq.dynamic_vortex_stretching (flow : NavierStokesFlow) (t : ℝ) : ℝ

Le véritable terme de Vortex Stretching dynamique.

Equations

• One or more equations did not get rendered due to their size.