Common microwave network components and composition

Shared matrix definitions and finite-index facts used by both synthesis models. Adapted from formalizing-analog-computing at commit a89c1e9263658c20a29046f9ed1a8eeb867dd537.

@[reducible, inline]

abbrev MiLAC.Network (n : ℕ) : Type

A matched network with n inputs and n outputs, represented by its transmission scattering matrix.

Equations

• MiLAC.Network n = Matrix (Fin n) (Fin n) ℂ

def MiLAC.interconnection : Network 1

An interconnection, directly connecting an input to an output.

Equations

• MiLAC.interconnection = 1

noncomputable def MiLAC.phaseShifter (φ : ℝ) : Network 1

A phase shifter with phase shift φ.

Equations

• MiLAC.phaseShifter φ x✝¹ x✝ = Complex.exp (↑φ * Complex.I)

def MiLAC.permutationNetwork {n : ℕ} (σ : Equiv.Perm (Fin n)) : Network n

A permutation network, reordering the signals according to σ.

Equations

• MiLAC.permutationNetwork σ = (Equiv.toPEquiv σ).toMatrix

theorem MiLAC.interconnection_eq_phaseShifter_zero : interconnection = phaseShifter 0

An interconnection is a phase shifter with zero phase.

Series and parallel composition

def MiLAC.series {n : ℕ} (A B : Network n) : Network n

The series of two networks, where A is followed by B.

Equations

• MiLAC.series A B = B * A

def MiLAC.parallel {n m : ℕ} (A : Network n) (B : Network m) : Network (n + m)

The parallel of two networks.

Equations

• MiLAC.parallel A B = (Matrix.reindex finSumFinEquiv finSumFinEquiv) (Matrix.fromBlocks A 0 0 B)

@[simp]

theorem MiLAC.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) : Fin.castAdd m i ≠ Fin.natAdd n j

The first and second blocks of a parallel network have disjoint ports.

@[simp]

theorem MiLAC.natAdd_ne_castAdd {n m : ℕ} (i : Fin m) (j : Fin n) : Fin.natAdd n i ≠ Fin.castAdd m j

Disjointness of parallel ports with the two blocks interchanged.

@[simp]

theorem MiLAC.parallel_castAdd_castAdd {n m : ℕ} (A : Network n) (B : Network m) (i j : Fin n) : parallel A B (Fin.castAdd m i) (Fin.castAdd m j) = A i j

The upper-left block of a parallel is the first network.

@[simp]

theorem MiLAC.parallel_castAdd_natAdd {n m : ℕ} (A : Network n) (B : Network m) (i : Fin n) (j : Fin m) : parallel A B (Fin.castAdd m i) (Fin.natAdd n j) = 0

The upper-right block of a parallel is zero.

@[simp]

theorem MiLAC.parallel_natAdd_castAdd {n m : ℕ} (A : Network n) (B : Network m) (i : Fin m) (j : Fin n) : parallel A B (Fin.natAdd n i) (Fin.castAdd m j) = 0

The lower-left block of a parallel is zero.

@[simp]

theorem MiLAC.parallel_natAdd_natAdd {n m : ℕ} (A : Network n) (B : Network m) (i j : Fin m) : parallel A B (Fin.natAdd n i) (Fin.natAdd n j) = B i j

The lower-right block of a parallel is the second network.

noncomputable def MiLAC.phaseDiagonal {n : ℕ} (φ : Fin n → ℝ) : Network n

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

Equations

• MiLAC.phaseDiagonal φ = Matrix.diagonal fun (i : Fin n) => Complex.exp (↑(φ i) * Complex.I)

Phase-only implementations

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

A network implementable with 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.

• 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.

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

A diagonal matrix of phases is implementable.