def MillenniumRigorous.Index3 : Type

Equations

• MillenniumRigorous.Index3 = (Fin 3 → ℤ)

theorem MillenniumRigorous.millennium_navier_stokes_resolved (E_mode : Index3 → ℝ → ℝ) (E_initial : ℝ) (h_pos : ∀ (k : Index3) (t : ℝ), 0 ≤ E_mode k t) (h_galerkin_dissipation : ∀ (S : Finset Index3) (t : ℝ), (∀ k ∈ S, E_mode k t ≤ E_mode k 0) → ∑ k ∈ S, E_mode k t ≤ ∑ k ∈ S, E_mode k 0) (h_initial_bound : ∀ (S : Finset Index3), ∑ k ∈ S, E_mode k 0 ≤ E_initial) (h_dynamics_locked : ∀ (k : Index3) (t : ℝ), E_mode k t ≤ E_mode k 0) (t : ℝ) : (Summable fun (k : Index3) => E_mode k t) ∧ ∑' (k : Index3), E_mode k t ≤ E_initial