The Lean 4 theorem `diagOp_hasZeroDeficiencyOn` in the `ChapterNavierStokesDeficiency` chapter of the timepiece formalization

-- Generated from ChapterNavierStokesDeficiency.lean — theorem BookProof.NavierStokesFlow.DiagonalEsa.diagOp_hasZeroDeficiencyOn
import Mathlib
import Definitions.Def_ChapterNavierStokesDeficiency
import Definitions.Def_ChapterAbelianDiagonalCountable
import Definitions.Def_ChapterNavierStokesEsa
import Definitions.Def_ChapterNavierStokesFlow
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.ChapterAbelianDiagonalCountable
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.DiagonalEsa


open scoped ENNReal

theorem BookProof.NavierStokesFlow.DiagonalEsa.diagOp_hasZeroDeficiencyOn (c : ℕ → ℝ) :
    HasZeroDeficiencyOn (lpFiniteModes ℕ) (diagOp c) := by sorry