`BookProof.ChapterHilbertSumIntertwine.memLp_fibrewise` (B : ∀ i, G i →L[ℂ] G i) (hB : ∀ i u, ‖B i u‖ ≤ ‖u‖) (w : lp G 2) : Memℓp (fun i => B i (w i)) 2
ProvedBookProof.ChapterHilbertSumIntertwine.memLp_fibrewisetheoremstimepiece
Prove the following Lean 4 theorem from ChapterHilbertSumIntertwine.
BookProof.ChapterHilbertSumIntertwine.memLp_fibrewise (B : ∀ i, G i →L[ℂ] G i) (hB : ∀ i u, ‖B i u‖ ≤ ‖u‖) (w : lp G 2) : Memℓp (fun i => B i (w i)) 2
Formalization note: Lean 4 identifier BookProof.ChapterHilbertSumIntertwine.memLp_fibrewise.
Preamble
-- Generated from ChapterHilbertSumIntertwine.lean — theorem BookProof.ChapterHilbertSumIntertwine.memℓp_fibrewise
import Mathlib
import Definitions.Def_ChapterHilbertSumIntertwine
open BookProof.ChapterHilbertSumIntertwine
open scoped InnerProductSpace
variable {ι : Type*}
variable {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)] [∀ i, InnerProductSpace ℂ (G i)]Formal statement
theorem BookProof.ChapterHilbertSumIntertwine.memLp_fibrewise (B : ∀ i, G i →L[ℂ] G i) (hB : ∀ i u, ‖B i u‖ ≤ ‖u‖)
(w : lp G 2) : Memℓp (fun i => B i (w i)) 2 := by sorry