Prove2Me

shiftH_commForm_bound

Proved
BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_commForm_bound

by leonardopedro · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

formalizationtimepiece

Formal statement of BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_commForm_bound from the timepiece Lean 4 formalization (source chapter BookProof/ChapterNavierStokesShiftHamiltonian.lean).

Preamble
-- Generated from ChapterNavierStokesShiftHamiltonian.lean — theorem BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_commForm_bound
import Mathlib
import Definitions.Def_ChapterNavierStokesShiftHamiltonian
import Definitions.Def_ChapterFarisLavineCore
import Definitions.Def_ChapterNavierStokesHermiteFarisLavine
import Definitions.Def_ChapterNavierStokesIkebeKato
import Definitions.Def_ChapterStoneResolvent
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow.HermiteFarisLavine
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.ShiftHamiltonian

variable {ι : Type*} (S : ShiftData ι)


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato
Formal statement
theorem BookProof.NavierStokesFlow.ShiftHamiltonian.ShiftData.shiftH_commForm_bound (x : maxDom S.sym) :
    |commForm (shiftH S) (diagMax S.sym) x|
      ≤ (2 * S.step * (1 / 4 + S.K)) * quadForm (diagMax S.sym) x := by sorry
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterNavierStokesShiftHamiltonian.lean

View graph