Computing with hybrid couplers and phase shifters

A network made of hybrid couplers and 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, hybridCoupler, 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 φₙ)).
• block: the 2 × 2 block D(θ₁₁, θ₁₂, θ₂₁), implementable with one hybrid coupler and three phase shifters.
• blockDiagonal: the block diagonal matrix of C blocks D(θ₁₁⁽ᶜ⁾, θ₁₂⁽ᶜ⁾, θ₂₁⁽ᶜ⁾) and S phases exp(j φₛ).
• Layer: a layer P_ℓ D_ℓ, made of a block diagonal matrix D_ℓ and a permutation matrix P_ℓ.
• layered: the product P_L D_L ⋯ P_1 D_1 P_0 of layers and an initial permutation matrix.
• dft: the N × N discrete Fourier transform (DFT) matrix.

Main results

• implementable_iff_layered: a network is implementable if and only if its transmission scattering matrix is P_L D_L ⋯ P_1 D_1 P_0, for some permutation matrices P_ℓ and block diagonal matrices D_ℓ.
• implementable_dft: the N × N DFT, with N = 2^L, is implementable.

noncomputable def MiLAC.HybridCouplersPhaseShifters.hybridCoupler : Network 2

A hybrid coupler, with transmission scattering matrix (1/√2) [[j, 1], [1, j]].

Equations

• MiLAC.HybridCouplersPhaseShifters.hybridCoupler = (1 / ↑√2) • !![Complex.I, 1; 1, Complex.I]

inductive MiLAC.HybridCouplersPhaseShifters.Implementable {n : ℕ} : Network n → Prop

A network implementable with hybrid couplers, interconnections, phase shifters, and permutation networks.

• ic : Implementable interconnection

  An interconnection is implementable.

• ps (φ : ℝ) : Implementable (phaseShifter φ)

  A phase shifter is implementable.

• pn {n : ℕ} (σ : Equiv.Perm (Fin n)) : Implementable (permutationNetwork σ)

  A permutation network is implementable.

• hc : Implementable hybridCoupler

  A hybrid coupler is implementable.

• series {n : ℕ} {A B : Network n} : Implementable A → Implementable B → Implementable (MiLAC.series A B)

  The series of two implementable networks is implementable.

• parallel {n m : ℕ} {A : Network n} {B : Network m} : Implementable A → Implementable B → Implementable (MiLAC.parallel A B)

  The parallel of two implementable networks is implementable.

Preliminary lemmas

theorem MiLAC.HybridCouplersPhaseShifters.permutationNetwork_mul {n : ℕ} (σ τ : Equiv.Perm (Fin n)) : permutationNetwork τ * permutationNetwork σ = permutationNetwork (σ * τ)

Permutation matrices multiply anti-homomorphically: P_τ P_σ = P_(σ * τ).

theorem MiLAC.HybridCouplersPhaseShifters.permutationNetwork_mul_eq_submatrix {n : ℕ} (σ : Equiv.Perm (Fin n)) (M : Network n) : permutationNetwork σ * M = Matrix.submatrix M (⇑σ) id

Left-multiplying by a permutation matrix permutes the rows.

theorem MiLAC.HybridCouplersPhaseShifters.mul_permutationNetwork_eq_submatrix {n : ℕ} (M : Network n) (σ : Equiv.Perm (Fin n)) : M * permutationNetwork σ = Matrix.submatrix M id ⇑(Equiv.symm σ)

Right-multiplying by a permutation matrix permutes the columns.

theorem MiLAC.HybridCouplersPhaseShifters.parallel_mul {n m : ℕ} (A B : Network n) (C D : Network m) : parallel A C * parallel B D = parallel (A * B) (C * D)

The product of two parallels is the parallel of the products.

theorem MiLAC.HybridCouplersPhaseShifters.parallel_permutationNetwork {n m : ℕ} (σ : Equiv.Perm (Fin n)) (τ : Equiv.Perm (Fin m)) : parallel (permutationNetwork σ) (permutationNetwork τ) = permutationNetwork (finSumFinEquiv.permCongr (Equiv.sumCongr σ τ))

The parallel of two permutation networks is a permutation network.

def MiLAC.HybridCouplersPhaseShifters.NetEquiv (X Y : (n : ℕ) × Network n) : Prop

Two networks (possibly of syntactically different sizes) are equal up to a relabelling of their ports.

Equations

• MiLAC.HybridCouplersPhaseShifters.NetEquiv X Y = ∃ (e : Fin X.fst ≃ Fin Y.fst), X.snd = Matrix.submatrix Y.snd ⇑e ⇑e

theorem MiLAC.HybridCouplersPhaseShifters.NetEquiv.trans {X Y Z : (n : ℕ) × Network n} (hXY : NetEquiv X Y) (hYZ : NetEquiv Y Z) : NetEquiv X Z

Equality up to a relabelling of the ports is transitive.

theorem MiLAC.HybridCouplersPhaseShifters.parallel_swap {n m : ℕ} (A : Network n) (B : Network m) : NetEquiv ⟨n + m, parallel A B⟩ ⟨m + n, parallel B A⟩

The parallel is commutative, up to a relabelling of the ports.

theorem MiLAC.HybridCouplersPhaseShifters.parallel_assoc {a b c : ℕ} (A : Network a) (B : Network b) (C : Network c) : NetEquiv ⟨a + b + c, parallel (parallel A B) C⟩ ⟨a + (b + c), parallel A (parallel B C)⟩

The parallel is associative, up to a relabelling of the ports.

theorem MiLAC.HybridCouplersPhaseShifters.NetEquiv.parallel_left {X Y : (n : ℕ) × Network n} (h : NetEquiv X Y) {a : ℕ} (A : Network a) : NetEquiv ⟨X.fst + a, parallel X.snd A⟩ ⟨Y.fst + a, parallel Y.snd A⟩

Equality up to a relabelling of the ports is preserved by placing a network below.

theorem MiLAC.HybridCouplersPhaseShifters.NetEquiv.reindex {n k : ℕ} (e : Fin k ≃ Fin n) (M : Network k) : NetEquiv ⟨n, (Matrix.reindex e e) M⟩ ⟨k, M⟩

A network is equal to its relabelling, up to a relabelling of the ports.

theorem MiLAC.HybridCouplersPhaseShifters.implementable_mul {n : ℕ} {A B : Network n} (hA : Implementable A) (hB : Implementable B) : Implementable (A * B)

The product of two implementable networks is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.implementable_submatrix {n : ℕ} {A : Network n} (hA : Implementable A) (σ τ : Equiv.Perm (Fin n)) : Implementable (Matrix.submatrix A ⇑σ ⇑τ)

Permuting the rows and the columns of an implementable network keeps it implementable.

def MiLAC.HybridCouplersPhaseShifters.ImplementableOn {ι : Type u_1} (M : Matrix ι ι ℂ) : Prop

A matrix is implementable on its index type if a finite port relabelling gives an implementable network. The relabelling witness rules out infinite index types.

Equations

• MiLAC.HybridCouplersPhaseShifters.ImplementableOn M = ∃ (n : ℕ) (e : ι ≃ Fin n), MiLAC.HybridCouplersPhaseShifters.Implementable ((Matrix.reindex e e) M)

theorem MiLAC.HybridCouplersPhaseShifters.not_implementableOn_of_infinite {ι : Type u_1} [Infinite ι] (M : Matrix ι ι ℂ) : ¬ImplementableOn M

An infinite collection of ports cannot be implemented by a finite network.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.of_equiv {ι : Type u_1} {M : Matrix ι ι ℂ} {m : ℕ} (g : ι ≃ Fin m) (h : Implementable ((Matrix.reindex g g) M)) : ImplementableOn M

An implementation after one relabelling witnesses implementability.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.to_equiv {ι : Type u_1} {M : Matrix ι ι ℂ} (h : ImplementableOn M) (n : ℕ) (e : ι ≃ Fin n) : Implementable ((Matrix.reindex e e) M)

An implementable matrix is implementable after any finite port relabelling.

theorem MiLAC.HybridCouplersPhaseShifters.implementableOn_iff {n : ℕ} (A : Network n) : ImplementableOn A ↔ Implementable A

For a network indexed by Fin n, ImplementableOn is Implementable.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.reindex {ι : Type u_1} {κ : Type u_2} {M : Matrix ι ι ℂ} (h : ImplementableOn M) (f : ι ≃ κ) : ImplementableOn ((Matrix.reindex f f) M)

Implementability is invariant under a relabelling of the ports.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.mul {ι : Type u_1} [Fintype ι] {A B : Matrix ι ι ℂ} (hA : ImplementableOn A) (hB : ImplementableOn B) : ImplementableOn (A * B)

The product of two implementable matrices is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.fromBlocks {ι : Type u_1} {κ : Type u_2} {A : Matrix ι ι ℂ} {B : Matrix κ κ ℂ} (hA : ImplementableOn A) (hB : ImplementableOn B) : ImplementableOn (Matrix.fromBlocks A 0 0 B)

A block diagonal matrix of two implementable matrices is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.implementableOn_of_isEmpty {ι : Type u_1} [IsEmpty ι] (M : Matrix ι ι ℂ) : ImplementableOn M

A matrix with no ports is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.blockDiagonal_one {m : Type u_1} (g : Fin 1 → Matrix m m ℂ) (h : ImplementableOn (g 0)) : ImplementableOn (Matrix.blockDiagonal g)

A block diagonal matrix with a single implementable block is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.blockDiagonal {m : Type u_1} (N : ℕ) (g : Fin N → Matrix m m ℂ) : (∀ (c : Fin N), ImplementableOn (g c)) → ImplementableOn (Matrix.blockDiagonal g)

A block diagonal matrix of implementable blocks is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.ImplementableOn.submatrix_symm {ι : Type u_1} {M : Matrix ι ι ℂ} (h : ImplementableOn M) {n : ℕ} (e₁ e₂ : ι ≃ Fin n) : Implementable (M.submatrix ⇑e₁.symm ⇑e₂.symm)

Relabelling the rows and the columns of an implementable matrix into Fin n independently gives an implementable network.

Characterization of implementable networks

noncomputable def MiLAC.HybridCouplersPhaseShifters.block (θ₁₁ θ₁₂ θ₂₁ : ℝ) : Network 2

The 2 × 2 block D(θ₁₁, θ₁₂, θ₂₁).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MiLAC.HybridCouplersPhaseShifters.blockDiagonal {C S : ℕ} (θ₁₁ θ₁₂ θ₂₁ : Fin C → ℝ) (φ : Fin S → ℝ) : Network (2 * C + S)

The block diagonal matrix diag(D(θ₁₁⁽¹⁾, θ₁₂⁽¹⁾, θ₂₁⁽¹⁾), …, D(θ₁₁⁽ᶜ⁾, θ₁₂⁽ᶜ⁾, θ₂₁⁽ᶜ⁾), exp(j φ₁), …, exp(j φ_S)).

Equations

• One or more equations did not get rendered due to their size.

structure MiLAC.HybridCouplersPhaseShifters.Layer (n : ℕ) : Type

A layer P_ℓ D_ℓ: a block diagonal matrix D_ℓ followed by a permutation matrix P_ℓ.

• C : ℕ

  The number of blocks of D_ℓ.

• S : ℕ

  The number of phases of D_ℓ.

• θ₁₁ : Fin self.C → ℝ

  The parameters θ₁₁ of the blocks of D_ℓ.

• θ₁₂ : Fin self.C → ℝ

  The parameters θ₁₂ of the blocks of D_ℓ.

• θ₂₁ : Fin self.C → ℝ

  The parameters θ₂₁ of the blocks of D_ℓ.

• φ : Fin self.S → ℝ

  The phases of D_ℓ.

• size : 2 * self.C + self.S = n

  D_ℓ has n ports.

• σ : Equiv.Perm (Fin n)

  The permutation of P_ℓ.

noncomputable def MiLAC.HybridCouplersPhaseShifters.layered {n : ℕ} (σ₀ : Equiv.Perm (Fin n)) : List (Layer n) → Network n

The product P_L D_L ⋯ P_1 D_1 P_0, with layers listed from L down to 1 (Matrix.reindex only renames the 2 C + S ports of D_ℓ as the n ports of the network).

Equations

• One or more equations did not get rendered due to their size.
• MiLAC.HybridCouplersPhaseShifters.layered σ₀ [] = MiLAC.permutationNetwork σ₀

Sufficiency

theorem MiLAC.HybridCouplersPhaseShifters.implementable_of_phaseShifters {n : ℕ} {A : Network n} (h : PhaseShifters.Implementable A) : Implementable A

Every phase-only implementation is also an implementation with hybrid couplers available.

theorem MiLAC.HybridCouplersPhaseShifters.implementable_if_phaseDiagonal {n : ℕ} (φ : Fin n → ℝ) : Implementable (phaseDiagonal φ)

A diagonal matrix of phases is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.implementable_if_block (θ₁₁ θ₁₂ θ₂₁ : ℝ) : Implementable (block θ₁₁ θ₁₂ θ₂₁)

A block D(θ₁₁, θ₁₂, θ₂₁) is implementable, with a phase shifter, a hybrid coupler, and two phase shifters in series.

theorem MiLAC.HybridCouplersPhaseShifters.implementable_if_blockDiagonal {C S : ℕ} (θ₁₁ θ₁₂ θ₂₁ : Fin C → ℝ) (φ : Fin S → ℝ) : Implementable (blockDiagonal θ₁₁ θ₁₂ θ₂₁ φ)

A block diagonal matrix is implementable.

theorem MiLAC.HybridCouplersPhaseShifters.implementable_if_layered {n : ℕ} (σ₀ : Equiv.Perm (Fin n)) (layers : List (Layer n)) : Implementable (layered σ₀ layers)

A network admitting a layered decomposition is implementable (sufficient condition).

Necessity

def MiLAC.HybridCouplersPhaseShifters.IsLayered {n : ℕ} (S : Network n) : Prop

A network admits a layered decomposition.

Equations

• MiLAC.HybridCouplersPhaseShifters.IsLayered S = ∃ (σ₀ : Equiv.Perm (Fin n)) (layers : List (MiLAC.HybridCouplersPhaseShifters.Layer n)), S = MiLAC.HybridCouplersPhaseShifters.layered σ₀ layers

theorem MiLAC.HybridCouplersPhaseShifters.isLayered_permutationNetwork {n : ℕ} (σ : Equiv.Perm (Fin n)) : IsLayered (permutationNetwork σ)

A permutation network admits a layered decomposition, with no layers.

theorem MiLAC.HybridCouplersPhaseShifters.isLayered_permutationNetwork_mul {n : ℕ} (τ σ₀ : Equiv.Perm (Fin n)) (layers : List (Layer n)) : IsLayered (permutationNetwork τ * layered σ₀ layers)

Left-multiplying a layered decomposition by a permutation matrix only changes its outermost permutation: σ₀ (if there are no layers) or the permutation of the topmost layer (if there are).

theorem MiLAC.HybridCouplersPhaseShifters.IsLayered.series {n : ℕ} {A B : Network n} (hA : IsLayered A) (hB : IsLayered B) : IsLayered (MiLAC.series A B)

The series of two networks admitting a layered decomposition admits one.

theorem MiLAC.HybridCouplersPhaseShifters.IsLayered.mul {n : ℕ} {A B : Network n} (hA : IsLayered A) (hB : IsLayered B) : IsLayered (A * B)

The product of two networks admitting a layered decomposition admits one.

theorem MiLAC.HybridCouplersPhaseShifters.IsLayered.of_netEquiv {X Y : (n : ℕ) × Network n} (h : NetEquiv X Y) (hY : IsLayered Y.snd) : IsLayered X.snd

Admitting a layered decomposition is invariant under a relabelling of the ports.

theorem MiLAC.HybridCouplersPhaseShifters.isLayered_blockDiagonal {C S : ℕ} (θ₁₁ θ₁₂ θ₂₁ : Fin C → ℝ) (φ : Fin S → ℝ) : IsLayered (blockDiagonal θ₁₁ θ₁₂ θ₂₁ φ)

A block diagonal matrix admits a layered decomposition, with one layer.

theorem MiLAC.HybridCouplersPhaseShifters.phaseDiagonal_parallel_one {n : ℕ} (φ : Fin n → ℝ) (m : ℕ) : parallel (phaseDiagonal φ) 1 = phaseDiagonal (Fin.append φ 0)

Placing an identity below a diagonal matrix of phases adds zero phases.

theorem MiLAC.HybridCouplersPhaseShifters.isLayered_parallel_blockDiagonal_one {n : ℕ} (layer : Layer n) (m : ℕ) : IsLayered (parallel ((Matrix.reindex (finCongr ⋯) (finCongr ⋯)) (blockDiagonal layer.θ₁₁ layer.θ₁₂ layer.θ₂₁ layer.φ)) 1)

Placing an identity below the block diagonal matrix of a layer gives a network admitting a layered decomposition.

theorem MiLAC.HybridCouplersPhaseShifters.IsLayered.parallel_one {n : ℕ} {S : Network n} (hS : IsLayered S) (m : ℕ) : IsLayered (MiLAC.parallel S 1)

Placing an identity below a network admitting a layered decomposition gives a network admitting one.

theorem MiLAC.HybridCouplersPhaseShifters.IsLayered.one_parallel {n : ℕ} {S : Network n} (hS : IsLayered S) (m : ℕ) : IsLayered (MiLAC.parallel 1 S)

Placing an identity above a network admitting a layered decomposition gives a network admitting one.

theorem MiLAC.HybridCouplersPhaseShifters.IsLayered.parallel {n m : ℕ} {A : Network n} {B : Network m} (hA : IsLayered A) (hB : IsLayered B) : IsLayered (MiLAC.parallel A B)

The parallel of two networks admitting a layered decomposition admits one.

theorem MiLAC.HybridCouplersPhaseShifters.isLayered_phaseShifter (φ : ℝ) : IsLayered (phaseShifter φ)

A phase shifter admits a layered decomposition, with one layer and a single phase.

theorem MiLAC.HybridCouplersPhaseShifters.isLayered_hybridCoupler : IsLayered hybridCoupler

A hybrid coupler admits a layered decomposition, with one layer and the single block D(π/2, 0, 0).

theorem MiLAC.HybridCouplersPhaseShifters.implementable_only_if_layered {n : ℕ} {S : Network n} (hS : Implementable S) : ∃ (σ₀ : Equiv.Perm (Fin n)) (layers : List (Layer n)), S = layered σ₀ layers

An implementable network admits a layered decomposition (necessary condition).

Main theorem

theorem MiLAC.HybridCouplersPhaseShifters.implementable_iff_layered {n : ℕ} {S : Network n} : Implementable S ↔ ∃ (σ₀ : Equiv.Perm (Fin n)) (layers : List (Layer n)), S = layered σ₀ layers

A network is implementable if and only if its transmission scattering matrix is P_L D_L ⋯ P_1 D_1 P_0, for some permutation matrices P_ℓ and block diagonal matrices D_ℓ.

Discrete Fourier transform

noncomputable def MiLAC.HybridCouplersPhaseShifters.dft (N : ℕ) : Network N

The N × N DFT matrix, [F_N]_{i,k} = ω^{ik} / √N with ω = exp(-j 2π / N) (indices start from 0 here, from 1 in the paper).

Equations

• MiLAC.HybridCouplersPhaseShifters.dft N i k = 1 / ↑√↑N * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑↑i * ↑↑k / ↑N)

noncomputable def MiLAC.HybridCouplersPhaseShifters.butterfly (L : ℕ) (i : Fin (2 ^ L)) : Matrix (Fin 2) (Fin 2) ℂ

The 2 × 2 butterfly blocks of the radix-2 FFT, (1/√2) [[1, ω^i], [1, -ω^i]] with ω = exp(-j 2π / 2^(L+1)).

Equations

• MiLAC.HybridCouplersPhaseShifters.butterfly L i a b = 1 / ↑√2 * ((-1) ^ (↑a * ↑b) * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑↑i * ↑↑b / 2 ^ (L + 1)))

theorem MiLAC.HybridCouplersPhaseShifters.butterfly_eq_block (L : ℕ) (i : Fin (2 ^ L)) : butterfly L i = block 0 (-2 * Real.pi * ↑↑i / 2 ^ (L + 1)) 0

Each butterfly block is a block D(0, -2π i / 2^(L+1), 0).

theorem MiLAC.HybridCouplersPhaseShifters.dft_exp (L a b i k : ℕ) : Complex.exp (-2 * ↑Real.pi * Complex.I * (↑i + 2 ^ L * ↑a) * (↑b + 2 * ↑k) / 2 ^ (L + 1)) = (-1) ^ (a * b) * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑i * ↑b / 2 ^ (L + 1)) * Complex.exp (-2 * ↑Real.pi * Complex.I * ↑i * ↑k / 2 ^ L)

The exponential identity behind the radix-2 decomposition of the DFT.

theorem MiLAC.HybridCouplersPhaseShifters.implementable_dft (L : ℕ) : Implementable (dft (2 ^ L))

The N × N DFT, with N = 2^L, is implementable with hybrid couplers and phase shifters (Corollary 3 in the paper).