`BookProof.ChapterCyclicDirectSum.starProjection_eq_of_hasSum` {ι : Type*} {V : ι → Submodule ℂ H} [∀ i, (V i).HasOrthogonalProjection] (hV : OrthogonalFamily ℂ (fun i => (V i)) fu

Proved

BookProof.ChapterCyclicDirectSum.starProjection_eq_of_hasSum

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterCyclicDirectSum.

BookProof.ChapterCyclicDirectSum.starProjection_eq_of_hasSum {ι : Type*} {V : ι → Submodule ℂ H} [∀ i, (V i).HasOrthogonalProjection] (hV : OrthogonalFamily ℂ (fun i => (V i)) fun i => (V i).subtypeₗᵢ) {c : ι → H} (hc : ∀ i, c i ∈ V i) {v : H} (h : HasSum c v) (j : ι) : (V j).starProjection v = c j

Formalization note: Lean 4 identifier BookProof.ChapterCyclicDirectSum.starProjection_eq_of_hasSum.

Preamble

-- Generated from ChapterCyclicDirectSum.lean — theorem BookProof.ChapterCyclicDirectSum.starProjection_eq_of_hasSum
import Definitions.Def_ChapterCyclicDecomposition
import Mathlib
import Definitions.Def_ChapterCyclicDirectSum
open BookProof.ChapterCyclicDirectSum


noncomputable section

open MeasureTheory Complex


open BookProof.ChapterCyclicDecomposition

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (T : H →L[ℂ] H) (hT : IsStarNormal T)

Formal statement

theorem BookProof.ChapterCyclicDirectSum.starProjection_eq_of_hasSum {ι : Type*} {V : ι → Submodule ℂ H}
    [∀ i, (V i).HasOrthogonalProjection]
    (hV : OrthogonalFamily ℂ (fun i => (V i)) fun i => (V i).subtypeₗᵢ)
    {c : ι → H} (hc : ∀ i, c i ∈ V i) {v : H} (h : HasSum c v) (j : ι) :
    (V j).starProjection v = c j := by sorry

View graph