theorem NavierStokes.helicity_local_bound (u_k omega_k : ℂ) : (u_k * star omega_k).re ≤ ‖u_k‖ * ‖omega_k‖

BRIQUE 1 : Borne locale fondamentale de l'hélicité. Prouve formellement que pour toute composante d'une fréquence k, la partie réelle de l'interaction u_k * ω_k* est inférieure ou égale au produit des modules.

theorem NavierStokes.helicity_vector_bound (u_k omega_k : Fin 3 → ℂ) : ∑ i : Fin 3, (u_k i * star (omega_k i)).re ≤ ∑ i : Fin 3, ‖u_k i‖ * ‖omega_k i‖

BRIQUE 2 : L'Inégalité de Cauchy-Schwarz vectorielle (3D). Prouve formellement que la somme des interactions sur les 3 axes de l'espace (x, y, z) est bornée par la somme des produits des modules. Cette brique permet de reconstruire le produit scalaire vectoriel.