`BookProof.ChapterLpRestrictSplit.restrictEmbed_add_restrictEmbed_compl` {A : Set α} (hA : MeasurableSet A) (u : Lp ℂ 2 mu) : restrictEmbed hA (restrictProj A u) + restrictEmbed hA

Proved

BookProof.ChapterLpRestrictSplit.restrictEmbed_add_restrictEmbed_compl

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterLpRestrictSplit.

BookProof.ChapterLpRestrictSplit.restrictEmbed_add_restrictEmbed_compl {A : Set α} (hA : MeasurableSet A) (u : Lp ℂ 2 mu) : restrictEmbed hA (restrictProj A u) + restrictEmbed hA.compl (restrictProj Aᶜ u) = u

Formalization note: Lean 4 identifier BookProof.ChapterLpRestrictSplit.restrictEmbed_add_restrictEmbed_compl.

Preamble

-- Generated from ChapterLpRestrictSplit.lean — theorem BookProof.ChapterLpRestrictSplit.restrictEmbed_add_restrictEmbed_compl
import Definitions.Def_ChapterLinftyMultiplication
import Mathlib
import Definitions.Def_ChapterLpRestrictSplit
open BookProof.ChapterLpRestrictSplit


noncomputable section

open MeasureTheory


open BookProof.ChapterLinftyMultiplication

variable {α : Type*} [MeasurableSpace α] {mu : Measure α}

Formal statement

theorem BookProof.ChapterLpRestrictSplit.restrictEmbed_add_restrictEmbed_compl {A : Set α} (hA : MeasurableSet A)
    (u : Lp ℂ 2 mu) :
    restrictEmbed hA (restrictProj A u) + restrictEmbed hA.compl (restrictProj Aᶜ u) = u := by sorry

View graph