`BookProof.ChapterF3.mehler_projector_matrix` (v xi xj : E') : inner (𝕜

Proved

BookProof.ChapterF3.mehler_projector_matrix

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterF3.

BookProof.ChapterF3.mehler_projector_matrix (v xi xj : E') : inner (𝕜

Formalization note: Lean 4 identifier BookProof.ChapterF3.mehler_projector_matrix.

Preamble

-- Generated from ChapterF3.lean —
import Mathlib
import Definitions.Def_ChapterF3
import Definitions.Def_ChapterGhostField
open BookProof.GhostField
open BookProof.ChapterF3


open scoped BigOperators
open Polynomial


noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
variable {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace ℂ E']

Formal statement

theorem BookProof.ChapterF3.mehler_projector_matrix (v xi xj : E') :
    inner (𝕜 := ℂ) xi (projOnto v xj)
      = (starRingEnd ℂ) (inner (𝕜 := ℂ) v xi) * inner (𝕜 := ℂ) v xj := by sorry

View graph