(i : Fin 3) : oscOp i = (creOp i).comp (annOp i) + ((1 / 2 : ℂ)) • LinearMap.id

Proved

BookProof.NavierStokesFlow.DiffFarisLavine.oscOp_eq_number

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

navier-stokesoperator-algebrastimepiece

Lean 4 theorem BookProof.NavierStokesFlow.DiffFarisLavine.oscOp_eq_number (module BookProof.NavierStokesFlow), source chapter BookProof/ChapterNavierStokesFlow.lean.

Preamble

-- Generated from ChapterNavierStokesDiffFarisLavine.lean — theorem BookProof.NavierStokesFlow.DiffFarisLavine.oscOp_eq_number
import Mathlib
import Definitions.Def_ChapterNavierStokesDiffFarisLavine
import Definitions.Def_ChapterHermiteProductCore
import Definitions.Def_ChapterHermiteProductBasis
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.DiffFarisLavine













open MvPolynomial
open BookProof.HermiteProductCore BookProof.HermiteProductBasis
open BookProof.NavierStokesFlow.LpNat BookProof.FarisLavine BookProof.NavierStokesFlow.IkebeKato BookProof.NavierStokesFlow.ThreeComponent BookProof.NavierStokesFlow.CanonicalVector BookProof.NavierStokesFlow.DifferentialL2

noncomputable section

set_option maxHeartbeats 4000000 in
-- The core operators unfold through several linear equivalences on a submodule of `L²(ℝ³)`,
-- so the default heartbeat budget is not enough.

Formal statement

theorem BookProof.NavierStokesFlow.DiffFarisLavine.oscOp_eq_number (i : Fin 3) :
    oscOp i = (creOp i).comp (annOp i) + ((1 / 2 : ℂ)) • LinearMap.id := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterNavierStokesFlow.lean

View graph