Prove2Me

`BookProof.ChapterF7.l2pair_sub_left` (f₁ fβ‚‚ g : 𝓒(ℝ, β„‚)) : l2pair (f₁ - fβ‚‚) g = l2pair f₁ g - l2pair fβ‚‚ g

Proved
BookProof.ChapterF7.l2pair_sub_left

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterF7.

BookProof.ChapterF7.l2pair_sub_left (f₁ fβ‚‚ g : 𝓒(ℝ, β„‚)) : l2pair (f₁ - fβ‚‚) g = l2pair f₁ g - l2pair fβ‚‚ g

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

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


open SchwartzMap MeasureTheory Complex
open scoped BigOperators


noncomputable section
Formal statement
theorem BookProof.ChapterF7.l2pair_sub_left (f₁ fβ‚‚ g : 𝓒(ℝ, β„‚)) :
    l2pair (f₁ - fβ‚‚) g = l2pair f₁ g - l2pair fβ‚‚ g := by sorry

View graph