Prove2Me

Lemma A.5 — L=(L∩M)⊕⊥(L∩(L∩M)⊥)=(L∩M)⊕⊥PLM⊥L=(L\cap M)\oplus^\perp(L\cap(L\cap M)^\perp)=(L\cap M)\oplus^\perp P_LM^\perp (real case)

Proved
NumInvQH.Oblique.lemma_A_5

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

linear-algebraorthogonal-projectionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let n∈Nn\in\mathbb N and let L,ML,M be linear subspaces of the Euclidean space Rn\mathbb R^n. Write X⊥\mathcal X^\perp for the orthogonal complement and PLP_L for the orthogonal projector onto LL. Then

L=(L∩M)⊕⊥(L∩(L∩M)⊥)=(L∩M)⊕⊥PLM⊥,L=(L\cap M)\oplus^\perp\bigl(L\cap(L\cap M)^\perp\bigr)=(L\cap M)\oplus^\perp P_LM^\perp,

where ⊕⊥\oplus^\perp is the orthogonal direct sum. The lemma describes the orthogonal complement of L∩ML\cap M inside LL as the projection of M⊥M^\perp onto LL; it is used with L=N(C)L=N(C), M=N(A)M=N(A) in the proof of Theorem A.4(4).

Formalization Note The paper states the lemma in Cn\mathbb C^n; this is its real specialisation, on EuclideanSpace ℝ (Fin n). Each orthogonal direct sum is stated as two facts: the sum of the two subspaces is LL, and they are orthogonal. PLP_L is Mathlib's Submodule.starProjection.

Preamble
import Mathlib
Formal statement
namespace NumInvQH.Oblique

/-- Lemma A.5, specialised from `ℂⁿ` to `ℝⁿ` (Euclidean space): for subspaces `L, M`,
`L = (L ∩ M) ⊕⊥ (L ∩ (L ∩ M)⊥) = (L ∩ M) ⊕⊥ P_L M⊥`, where `P_L` is the orthogonal projector
onto `L`. Each orthogonal direct sum is stated as "the sum equals `L` and the two summands are
orthogonal". -/
theorem lemma_A_5 {n : ℕ} (L M : Submodule ℝ (EuclideanSpace ℝ (Fin n))) :
    let PL : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin n) := L.starProjection
    (L ⊓ M) ⊔ (L ⊓ (L ⊓ M)ᗮ) = L ∧ (L ⊓ M) ⟂ (L ⊓ (L ⊓ M)ᗮ) ∧
    (L ⊓ M) ⊔ Mᗮ.map PL = L ∧ (L ⊓ M) ⟂ Mᗮ.map PL := by sorry

end NumInvQH.Oblique
Source
Černý, Czichowsky & Kallsen, Numeraire-invariant quadratic hedging and mean–variance portfolio allocation, arXiv:2110.09416v4, p. 28, Lemma A.5
Human review

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph