Computing with phase shifters

A network made of phase shifters, interconnected through interconnections and permutation networks, and connected in series and in parallel, is represented by its transmission scattering matrix (Network n).

Main definitions

• interconnection, phaseShifter, permutationNetwork: the components.
• series, parallel: series and parallel connection of two networks.
• Implementable: the networks obtainable from the components by series and parallel connections.
• phaseDiagonal: the diagonal matrix diag(exp(j φ₁), …, exp(j φₙ)).
• permutedPhaseDiagonal: the product P_σ diag(exp(j φ₁), …, exp(j φₙ)) of a permutation matrix and a diagonal matrix of phases.

Main results

• implementable_iff_permutedPhaseDiagonal: a network is implementable if and only if its transmission scattering matrix is a permutation matrix times a diagonal matrix of phases.

Characterization of implementable networks

noncomputable def MiLAC.PhaseShifters.permutedPhaseDiagonal {n : ℕ} (φ : Fin n → ℝ) (σ : Equiv.Perm (Fin n)) : Network n

The permuted diagonal matrix P_σ diag(exp(j φ₁), …, exp(j φₙ)).

Equations

• MiLAC.PhaseShifters.permutedPhaseDiagonal φ σ = (Equiv.toPEquiv σ).toMatrix * Matrix.diagonal fun (i : Fin n) => Complex.exp (↑(φ i) * Complex.I)

@[simp]

theorem MiLAC.PhaseShifters.permutedPhaseDiagonal_apply {n : ℕ} (φ : Fin n → ℝ) (σ : Equiv.Perm (Fin n)) (i j : Fin n) : permutedPhaseDiagonal φ σ i j = if σ i = j then Complex.exp (↑(φ (σ i)) * Complex.I) else 0

An entry of a permuted phase diagonal has at most one nonzero value per row.

Sufficiency

theorem MiLAC.PhaseShifters.implementable_if_permutedPhaseDiagonal {n : ℕ} (φ : Fin n → ℝ) (σ : Equiv.Perm (Fin n)) : Implementable (permutedPhaseDiagonal φ σ)

A permuted diagonal matrix of phases is implementable (sufficient condition).

Necessity

theorem MiLAC.PhaseShifters.series_permutedPhaseDiagonal {n : ℕ} (φ ψ : Fin n → ℝ) (σ τ : Equiv.Perm (Fin n)) : ∃ (χ : Fin n → ℝ) (ρ : Equiv.Perm (Fin n)), series (permutedPhaseDiagonal φ σ) (permutedPhaseDiagonal ψ τ) = permutedPhaseDiagonal χ ρ

The series of two permuted diagonal matrices is a permuted diagonal matrix.

theorem MiLAC.PhaseShifters.parallel_permutedPhaseDiagonal {n m : ℕ} (φ : Fin n → ℝ) (ψ : Fin m → ℝ) (σ : Equiv.Perm (Fin n)) (τ : Equiv.Perm (Fin m)) : ∃ (χ : Fin (n + m) → ℝ) (ρ : Equiv.Perm (Fin (n + m))), parallel (permutedPhaseDiagonal φ σ) (permutedPhaseDiagonal ψ τ) = permutedPhaseDiagonal χ ρ

The parallel of two permuted diagonal matrices is a permuted diagonal matrix.

theorem MiLAC.PhaseShifters.implementable_only_if_permutedPhaseDiagonal {n : ℕ} {S : Network n} (hS : Implementable S) : ∃ (φ : Fin n → ℝ) (σ : Equiv.Perm (Fin n)), S = permutedPhaseDiagonal φ σ

An implementable network is a permuted diagonal matrix of phases (necessary condition).

Main theorem

theorem MiLAC.PhaseShifters.implementable_iff_permutedPhaseDiagonal {n : ℕ} {S : Network n} : Implementable S ↔ ∃ (φ : Fin n → ℝ) (σ : Equiv.Perm (Fin n)), S = permutedPhaseDiagonal φ σ

A network is implementable if and only if it is a permuted diagonal matrix of phases.