`BookProof.NavierStokesFlow.AffineBlock.affFun_embFun` (κ c : J → ℝ) (hκ : ∀ j, 0 ≤ κ j) (hc : ∀ j, 0 ≤ c j) (j : J) (a : ℕ → ℂ) : affFun κ c hκ hc (embFun j a) = embFun j...

Proved

BookProof.NavierStokesFlow.AffineBlock.affFun_embFun

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNavierStokesAffineBlockEsa.

BookProof.NavierStokesFlow.AffineBlock.affFun_embFun (κ c : J → ℝ) (hκ : ∀ j, 0 ≤ κ j) (hc : ∀ j, 0 ≤ c j) (j : J) (a : ℕ → ℂ) : affFun κ c hκ hc (embFun j a) = embFun j (fun n => (affData (hκ j) (hc j)).fst.hFun a n + (affData (hκ j) (hc j)).snd.hFun a n)

Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.AffineBlock.affFun_embFun.

Preamble

-- Generated from ChapterNavierStokesAffineBlockEsa.lean — theorem BookProof.NavierStokesFlow.AffineBlock.affFun_embFun
import Mathlib
import Definitions.Def_ChapterNavierStokesAffineBlockEsa
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
import Definitions.Def_ChapterNavierStokesHermiteFarisLavine
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.AffineFiber.PairShift
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.AffineBlock


open scoped ENNReal



open LpNat BookProof.FarisLavine IkebeKato HermiteFarisLavine ShiftHamiltonian AffineFiber BilinearEsa

variable {J : Type*}

Formal statement

theorem BookProof.NavierStokesFlow.AffineBlock.affFun_embFun (κ c : J → ℝ) (hκ : ∀ j, 0 ≤ κ j) (hc : ∀ j, 0 ≤ c j)
    (j : J) (a : ℕ → ℂ) :
    affFun κ c hκ hc (embFun j a)
      = embFun j (fun n => (affData (hκ j) (hc j)).fst.hFun a n
          + (affData (hκ j) (hc j)).snd.hFun a n) := by sorry

View graph