Imports
Harmonic Wave
Time-harmonic waves.
Note TODO EGU3E may require considerable effort to be made rigorous and may heavily depend on
the status of Fourier theory in Mathlib.
@[ expose ] public section
The wavevector which indicates a direction and has magnitude 2π/λ.
abbrev WaveVector ( d : ℕ := 3 ) := EuclideanSpace ℝ ( Fin d )
TODO "Show that the wave equation is invariant under rotations and any direction `s`
can be rotated to `EuclideanSpace.single 2 1` if only one wave is concerned."
Transverse monochromatic time-harmonic plane wave where the direction of propagation
is taken to be EuclideanSpace.single 2 1. f₀x and f₀y are the respective amplitudes,
ω is the angular frequency, δx and δy are the respective phases for fx and fy.
set_option linter.unusedVariables false in @[ nolint unusedArguments ]
noncomputable def transverseHarmonicPlaneWave ( k : WaveVector ) ( f₀x f₀y ω δx δy : ℝ )
( hk : k = EuclideanSpace.single 2 ( ω / c ) ) :
Time → Space → EuclideanSpace ℝ ( Fin 3 ) :=
let fx := harmonicWave ( fun _ _ => f₀x ) ( fun _ r => ⟪ k , basis . repr r ⟫_ ℝ - δx ) ( fun _ => ω ) k
let fy := harmonicWave ( fun _ _ => f₀y ) ( fun _ r => ⟪ k , basis . repr r ⟫_ ℝ - δy ) ( fun _ => ω ) k
fun t r => fx t r • EuclideanSpace.single 0 1 + fy t r • EuclideanSpace.single 1 1
The transverse harmonic planewave representation is equivalent to the general planewave
expression with ‖k‖ = ω/c.
lemma transverseHarmonicPlaneWave_eq_planeWave { c : ℝ } { k : WaveVector } { f₀x f₀y ω δx δy : ℝ }
( hc_ge_zero : 0 < c ) ( hω_ge_zero : 0 < ω ) ( hk : k = EuclideanSpace.single 2 ( ω / c ) ) :
( transverseHarmonicPlaneWave k f₀x f₀y ω δx δy hk ) = planeWave
( fun p => ( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • ( EuclideanSpace.single 0 1 ) +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • ( EuclideanSpace.single 1 1 ) ) c
( WaveVector.toDirection k ( by c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) ⊢ k ≠ 0 rw [ hk c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) ⊢ EuclideanSpace.single 2 ( ω / c ) ≠ 0 c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) ⊢ EuclideanSpace.single 2 ( ω / c ) ≠ 0 ] c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) ⊢ EuclideanSpace.single 2 ( ω / c ) ≠ 0 ; simp [ ne_of_gt , hc_ge_zero , hω_ge_zero ] All goals completed! 🐙 ) ) := by c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) ⊢ transverseHarmonicPlaneWave k f₀x f₀y ω δx δy hk =
planeWave
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
c ( k . toDirection ⋯ )
unfold transverseHarmonicPlaneWave planeWave c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) ⊢ (have fx := harmonicWave (fun x x_1 => f₀x ) (fun x r => ⟪ k , basis . repr r ⟫_ ℝ - δx ) (fun x => ω ) k ;
have fy := harmonicWave (fun x x_1 => f₀y ) (fun x r => ⟪ k , basis . repr r ⟫_ ℝ - δy ) (fun x => ω ) k ;
fun t r => fx t r • EuclideanSpace.single 0 1 + fy t r • EuclideanSpace.single 1 1 ) =
fun t x =>
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ x , ( k . toDirection ⋯ ) . unit 3 ⟫_ ℝ - c * t . val )
ext1 t c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time ⊢ (fun r =>
harmonicWave (fun x x_1 => f₀x ) (fun x r => ⟪ k , basis . repr r ⟫_ ℝ - δx ) (fun x => ω ) k t r •
EuclideanSpace.single 0 1 +
harmonicWave (fun x x_1 => f₀y ) (fun x r => ⟪ k , basis . repr r ⟫_ ℝ - δy ) (fun x => ω ) k t r •
EuclideanSpace.single 1 1 ) =
fun x =>
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ x , ( k . toDirection ⋯ ) . unit 3 ⟫_ ℝ - c * t . val )
ext1 r c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ harmonicWave (fun x x_1 => f₀x ) (fun x r => ⟪ k , basis . repr r ⟫_ ℝ - δx ) (fun x => ω ) k t r • EuclideanSpace.single 0 1 +
harmonicWave (fun x x_1 => f₀y ) (fun x r => ⟪ k , basis . repr r ⟫_ ℝ - δy ) (fun x => ω ) k t r •
EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , ( k . toDirection ⋯ ) . unit 3 ⟫_ ℝ - c * t . val )
rw [ harmonicWave , c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
harmonicWave (fun x x_1 => f₀y ) (fun x r => ⟪ k , basis . repr r ⟫_ ℝ - δy ) (fun x => ω ) k t r •
EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , ( k . toDirection ⋯ ) . unit 3 ⟫_ ℝ - c * t . val ) c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , { unit := ‖ k ‖ ⁻¹ • basis . repr . symm k , norm := ⋯ } . unit 3 ⟫_ ℝ - c * t . val ) harmonicWave , c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , ( k . toDirection ⋯ ) . unit 3 ⟫_ ℝ - c * t . val ) c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , { unit := ‖ k ‖ ⁻¹ • basis . repr . symm k , norm := ⋯ } . unit 3 ⟫_ ℝ - c * t . val ) WaveVector.toDirection c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , { unit := ‖ k ‖ ⁻¹ • basis . repr . symm k , norm := ⋯ } . unit 3 ⟫_ ℝ - c * t . val ) c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , { unit := ‖ k ‖ ⁻¹ • basis . repr . symm k , norm := ⋯ } . unit 3 ⟫_ ℝ - c * t . val ) ] c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
( ⟪ r , { unit := ‖ k ‖ ⁻¹ • basis . repr . symm k , norm := ⋯ } . unit 3 ⟫_ ℝ - c * t . val )
simp only [ Fin.isValue , neg_mul ] c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1
have normk : ‖ k ‖ = ω / c := by c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) ⊢ transverseHarmonicPlaneWave k f₀x f₀y ω δx δy hk =
planeWave
(fun p =>
( f₀x * Real.cos ( - ( ω / c ) * p + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c ) * p + δy ) ) • EuclideanSpace.single 1 1 )
c ( k . toDirection ⋯ ) c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1
rw [ hk c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ‖ EuclideanSpace.single 2 ( ω / c ) ‖ = ω / c c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ‖ EuclideanSpace.single 2 ( ω / c ) ‖ = ω / c c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1 ] c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space ⊢ ‖ EuclideanSpace.single 2 ( ω / c ) ‖ = ω / c c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1
simp [ ← abs_div , hc_ge_zero , hω_ge_zero , le_of_lt ] c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1 c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ‖ k ‖ ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1
rw [ normk c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1 c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1 ] c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - c * t . val ) ) + δy ) ) • EuclideanSpace.single 1 1
rw [ mul_sub , c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ⟪ r , ( ω / c ) ⁻¹ • basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 inner_smul_right , c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ k , basis . repr r ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ ) - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ ) - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 real_inner_comm , c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ ) - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ ) - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 ← mul_assoc c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1 ] c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δx ) ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ( ⟪ basis . repr r , k ⟫_ ℝ - δy ) ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( - ( ω / c * ( ω / c ) ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ - ω / c * ( c * t . val ) ) + δy ) ) •
EuclideanSpace.single 1 1
ring_nf c : ℝ k : WaveVector f₀x : ℝ f₀y : ℝ ω : ℝ δx : ℝ δy : ℝ hc_ge_zero : 0 < c hω_ge_zero : 0 < ω hk : k = EuclideanSpace.single 2 ( ω / c ) t : Time r : Space normk : ‖ k ‖ = ω / c ⊢ ( f₀x * Real.cos ( ω * t . val - ⟪ basis . repr r , k ⟫_ ℝ + δx ) ) • EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val - ⟪ basis . repr r , k ⟫_ ℝ + δy ) ) • EuclideanSpace.single 1 1 =
( f₀x * Real.cos ( ω * t . val * c * c ⁻¹ - ω * c ⁻¹ * ω ⁻¹ * c ⁻¹ ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ + δx ) ) •
EuclideanSpace.single 0 1 +
( f₀y * Real.cos ( ω * t . val * c * c ⁻¹ - ω * c ⁻¹ * ω ⁻¹ * c ⁻¹ ⁻¹ * ⟪ r , basis . repr . symm k ⟫_ ℝ + δy ) ) •
EuclideanSpace.single 1 1
simp [ ne_of_gt , hc_ge_zero , hω_ge_zero , mul_comm ω , mul_assoc , basis_repr_inner_eq ] All goals completed! 🐙
TODO "Show that any disturbance (subject to certain conditions) can be expressed
as a superposition of harmonic plane waves via Fourier integral."