Polarization

In this file the real representation is used to develop representations of polarizations such as the polarization ellipse, Stokes parameters and the Poincaré sphere for monochromatic time-harmonic electromagnetic plane waves.

More general definitions that can be applied to a wider range of situations will be shown to be equivalent to the definitions in this file where appropriate.

Monochromatic wave

noncomputable def Optics.monochromX (k : ClassicalMechanics.WaveVector) (E₀x ω δx : ℝ) : Time → Space → ℝ

x-component of monochromatic time-harmonic wave.

Equations

• Optics.monochromX k E₀x ω δx = ClassicalMechanics.harmonicWave (fun (x : ℝ) (x : Space) => E₀x) (fun (x : ℝ) (r : Space) => inner ℝ k r - δx) (fun (x : ClassicalMechanics.WaveVector) => ω) k

noncomputable def Optics.monochromY (k : ClassicalMechanics.WaveVector) (E₀y ω δy : ℝ) : Time → Space → ℝ

y-component of monochromatic time-harmonic wave.

Equations

• Optics.monochromY k E₀y ω δy = ClassicalMechanics.harmonicWave (fun (x : ℝ) (x : Space) => E₀y) (fun (x : ℝ) (r : Space) => inner ℝ k r - δy) (fun (x : ClassicalMechanics.WaveVector) => ω) k

noncomputable def Optics.harmonicElectromagneticPlaneWave {c : ℝ} (k : ClassicalMechanics.WaveVector) (E₀x E₀y ω δx δy : ℝ) (hk : k = EuclideanSpace.single 2 (ω / c)) : Electromagnetism.ElectricField

General form of monochromatic time-harmonic electromagnetic plane wave where the direction of propagation is taken to be EuclideanSpace.single 2 1. E₀x and E₀y are the respective amplitudes, ω is the angular frequency, δx and δy are the respective phases for Ex and Ey.

Equations

• Optics.harmonicElectromagneticPlaneWave k E₀x E₀y ω δx δy hk t r = Optics.monochromX k E₀x ω δx t r • EuclideanSpace.single 0 1 + Optics.monochromY k E₀y ω δy t r • EuclideanSpace.single 1 1

theorem Optics.harmonicElectromagneticPlaneWave_eq_electricplaneWave {c : ℝ} {k : ClassicalMechanics.WaveVector} {E₀x E₀y ω δx δy : ℝ} (hc_ge_zero : 0 < c) (hω_ge_zero : 0 < ω) (hk : k = EuclideanSpace.single 2 (ω / c)) : harmonicElectromagneticPlaneWave k E₀x E₀y ω δx δy hk = Electromagnetism.electricPlaneWave (fun (p : ℝ) => (E₀x * Real.cos (-(ω / c) * p + δx)) • EuclideanSpace.single 0 1 + (E₀y * Real.cos (-(ω / c) * p + δy)) • EuclideanSpace.single 1 1) c (k.toDirection ⋯)

The transverse harmonic planewave representation is equivalent to the general electric field planewave expression with ‖k‖ = ω/c.

Polarization ellipse

theorem Optics.eq_monochromX {k : ClassicalMechanics.WaveVector} {E₀x τ ω δx : ℝ} {t : Time} {r : Space} (h : τ = ω * t - inner ℝ k r) : monochromX k E₀x ω δx t r = E₀x * Real.cos (τ + δx)

monochromX is equivalent to E₀x * cos (τ + δx) with τ = ω * t - inner ℝ k r.

theorem Optics.eq_monochromY {k : ClassicalMechanics.WaveVector} {E₀y τ ω δy : ℝ} {t : Time} {r : Space} (h : τ = ω * t - inner ℝ k r) : monochromY k E₀y ω δy t r = E₀y * Real.cos (τ + δy)

monochromY is equivalent to E₀y * cos (τ + δy) with τ = ω * t - inner ℝ k r.

theorem Optics.polarizationEllipse {k : ClassicalMechanics.WaveVector} {E₀x E₀y τ ω δx δy : ℝ} {t : Time} {r : Space} (hx : E₀x ≠ 0) (hy : E₀y ≠ 0) (h : τ = ω * t - inner ℝ k r) : (monochromX k E₀x ω δx t r / E₀x) ^ 2 + (monochromY k E₀y ω δy t r / E₀y) ^ 2 - 2 * (monochromX k E₀x ω δx t r / E₀x) * (monochromY k E₀y ω δy t r / E₀y) * Real.cos (δy - δx) = Real.sin (δy - δx) ^ 2

The locus of the electric field vector of an monochromatic time-harmonic electromagnetic plane wave is an ellipse.