QR Decomposition and its Product

Stream: new members

[Nick_adfor]

Can QR Decomposition and its Product be formalized by lean? I do not even find QR Decomposition in lean : (

Problem Statement

Given a function f: Mₙ(ℂ) → Mₙ(ℂ) that maps each invertible complex square matrix A to its unique QR decomposition (Q, R), where:

1. A = QR
2. Q is unitary (i.e., Q*Q = I)
3. R is upper triangular with positive real diagonal elements

We need to prove that this function f preserves multiplication, i.e., for any two invertible matrices A and B in Mₙ(ℂ):
f(AB) = f(A)f(B)

Proof Approach

To prove that f preserves multiplication, we need to show that the QR decomposition of AB equals the QR decomposition of the product of their respective QR decompositions. Here are the detailed steps:

1. Let A = Qᴬ Rᴬ and B = Qᴮ Rᴮ be the QR decompositions of A and B respectively
2. Then AB = Qᴬ Rᴬ Qᴮ Rᴮ
3. Let C = Rᴬ Qᴮ, which is invertible (since both Rᴬ and Qᴮ are invertible)
4. Perform QR decomposition on C: C = Qᶜ Rᶜ
5. Therefore AB = Qᴬ Qᶜ Rᶜ Rᴮ
6. Note that Qᴬ Qᶜ is a product of unitary matrices, hence still unitary
7. Rᶜ Rᴮ is a product of upper triangular matrices, hence still upper triangular with positive real diagonal elements (since both Rᶜ and Rᴮ have positive real diagonal elements)
8. By the uniqueness of QR decomposition, this must be the QR decomposition of AB
9. Therefore f(AB) = (Qᴬ Qᶜ, Rᶜ Rᴮ)
10. And f(A)f(B) = (Qᴬ, Rᴬ)(Qᴮ, Rᴮ) = (Qᴬ Qᶜ, Rᶜ Rᴮ) (because the QR decomposition of Rᴬ Qᴮ is (Qᶜ, Rᶜ))

Thus we've proved that f(AB) = f(A)f(B).