`BookProof.ChapterF4.countSketch_add` (hash : α → κ) (s : α → Ω → ℝ) (x y : α → ℝ) (ω : Ω) (h : κ) : countSketch hash s (x + y) ω h = countSketch hash s x ω h + countSketch...
ProvedBookProof.ChapterF4.countSketch_addtheoremstimepiece
Prove the following Lean 4 theorem from ChapterF4.
BookProof.ChapterF4.countSketch_add (hash : α → κ) (s : α → Ω → ℝ) (x y : α → ℝ) (ω : Ω) (h : κ) : countSketch hash s (x + y) ω h = countSketch hash s x ω h + countSketch hash s y ω h
Formalization note: Lean 4 identifier BookProof.ChapterF4.countSketch_add.
Preamble
-- Generated from ChapterF4.lean — theorem BookProof.ChapterF4.countSketch_add
import Mathlib
import Definitions.Def_ChapterF4
open BookProof.ChapterF4
open scoped BigOperators Matrix
variable {d k : ℕ}
variable {A : Type*} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [ContinuousStar A]
[CompleteSpace A] [StarModule ℂ A]
variable {α κ Ω : Type*} [Fintype α] [DecidableEq α] [Fintype κ] [DecidableEq κ]
{mΩ : MeasurableSpace Ω}Formal statement
theorem BookProof.ChapterF4.countSketch_add (hash : α → κ) (s : α → Ω → ℝ) (x y : α → ℝ) (ω : Ω) (h : κ) :
countSketch hash s (x + y) ω h = countSketch hash s x ω h + countSketch hash s y ω h := by sorry