Prove2Me

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

Proved
BookProof.ChapterF7.l2pair_sub_right

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterF7.

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

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

Preamble
-- Generated from ChapterF7.lean β€” theorem BookProof.ChapterF7.l2pair_sub_right
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_right (f g₁ gβ‚‚ : 𝓒(ℝ, β„‚)) :
    l2pair f (g₁ - gβ‚‚) = l2pair f g₁ - l2pair f gβ‚‚ := by sorry

View graph