Prove2Me

`BookProof.NavierStokesFlow.MomentumPerturbation.pertHam_commForm_bound` (c : ι → ℝ) (hc : ∀ k, 1 ≤ c k) (u w : maxDom c) (x : maxDom c) : |commForm (pertHam c (u : L2I ι) (w : L2I

Proved
BookProof.NavierStokesFlow.MomentumPerturbation.pertHam_commForm_bound

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesMomentumPerturbation.

BookProof.NavierStokesFlow.MomentumPerturbation.pertHam_commForm_bound (c : ι → ℝ) (hc : ∀ k, 1 ≤ c k) (u w : maxDom c) (x : maxDom c) : |commForm (pertHam c (u : L2I ι) (w : L2I ι)) (diagMax c) x| ≤ (2 * (‖(u : L2I ι)‖ * ‖diagMax c w‖ + ‖(w : L2I ι)‖ * ‖diagMax c u‖)) * quadForm (diagMax c) x

Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.MomentumPerturbation.pertHam_commForm_bound.

Preamble
-- Generated from ChapterNavierStokesMomentumPerturbation.lean — theorem BookProof.NavierStokesFlow.MomentumPerturbation.pertHam_commForm_bound
import Mathlib
import Definitions.Def_ChapterNavierStokesMomentumPerturbation
import Definitions.Def_ChapterFarisLavineCore
import Definitions.Def_ChapterNavierStokesIkebeKato
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.MomentumPerturbation




open LpNat BookProof.FarisLavine IkebeKato

variable {ι : Type*}
Formal statement
theorem BookProof.NavierStokesFlow.MomentumPerturbation.pertHam_commForm_bound (c : ι → ℝ) (hc : ∀ k, 1 ≤ c k) (u w : maxDom c)
    (x : maxDom c) :
    |commForm (pertHam c (u : L2I ι) (w : L2I ι)) (diagMax c) x|
      ≤ (2 * (‖(u : L2I ι)‖ * ‖diagMax c w‖ + ‖(w : L2I ι)‖ * ‖diagMax c u‖))
        * quadForm (diagMax c) x := by sorry

View graph