Prove2Me

`BookProof.ChapterF7.i_comm_l2Symmetric` {K V : 𝓒(ℝ, β„‚) β†’L[β„‚] 𝓒(ℝ, β„‚)} (hK : IsL2Symmetric K) (hV : IsL2Symmetric V) : IsL2Symmetric (Complex.I β€’ (K.comp V - V.comp K))

Proved
BookProof.ChapterF7.i_comm_l2Symmetric

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterF7.

BookProof.ChapterF7.i_comm_l2Symmetric {K V : 𝓒(ℝ, β„‚) β†’L[β„‚] 𝓒(ℝ, β„‚)} (hK : IsL2Symmetric K) (hV : IsL2Symmetric V) : IsL2Symmetric (Complex.I β€’ (K.comp V - V.comp K))

Formalization note: Lean 4 identifier BookProof.ChapterF7.i_comm_l2Symmetric.

Preamble
-- Generated from ChapterF7.lean β€” theorem BookProof.ChapterF7.i_comm_l2Symmetric
import Mathlib
import Definitions.Def_ChapterF7
open BookProof.ChapterF7


open SchwartzMap MeasureTheory Complex
open scoped BigOperators


noncomputable section
Formal statement
theorem BookProof.ChapterF7.i_comm_l2Symmetric {K V : 𝓒(ℝ, β„‚) β†’L[β„‚] 𝓒(ℝ, β„‚)}
    (hK : IsL2Symmetric K) (hV : IsL2Symmetric V) :
    IsL2Symmetric (Complex.I β€’ (K.comp V - V.comp K)) := by sorry

View graph