(d : ℕ) (p q : Fin d → ℕ → ℝ) : HasZeroDeficiencyOn (lpFiniteModes ℕ) (diagComparisonData d p q).comparison
ProvedBookProof.NavierStokesFlow.FarisLavineLift.diagComparison_hasZeroDeficiencyOnnavier-stokesoperator-algebrastimepiece
Lean 4 theorem BookProof.NavierStokesFlow.FarisLavineLift.diagComparison_hasZeroDeficiencyOn (module BookProof.NavierStokesFlow), source chapter BookProof/ChapterNavierStokesFlow.lean.
Preamble
-- Generated from ChapterNavierStokesFarisLavineLift.lean — theorem BookProof.NavierStokesFlow.FarisLavineLift.diagComparison_hasZeroDeficiencyOn
import Mathlib
import Definitions.Def_ChapterNavierStokesFarisLavineLift
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.FarisLavineLift
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {d : ℕ} (c : ComparisonData F d)Formal statement
theorem BookProof.NavierStokesFlow.FarisLavineLift.diagComparison_hasZeroDeficiencyOn (d : ℕ) (p q : Fin d → ℕ → ℝ) :
HasZeroDeficiencyOn (lpFiniteModes ℕ) (diagComparisonData d p q).comparison := by sorrySource