Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersClassicalMechanics.transverseHarmonicPlaneWave_eq_planeWave
Plain-language statement
The transverse harmonic planewave representation is equivalent to the general planewave expression with ‖k‖ = ω/c.
Source project: Physlib
Person-level attribution pending.
Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_space_deriv_same
Project documentation
The electromagnetic potential for a Harmonic wave travelling in the x-direction with wave number k. -/ noncomputable def harmonicWaveX (𝓕 : FreeSpace) (k : ℝ) (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) : ElectromagneticPotential d.succ where val := fun x μ => match μ with | Sum.inl 0 => 0 | Sum.inr 0 => 0 | Sum.inr ⟨Nat.succ i, h⟩ => -E₀ ⟨i, Nat.succ_lt_succ_i...
Source project: Physlib
Person-level attribution pending.
Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ_time_deriv
Project documentation
The electromagnetic potential for a Harmonic wave travelling in the x-direction with wave number k. -/ noncomputable def harmonicWaveX (𝓕 : FreeSpace) (k : ℝ) (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) : ElectromagneticPotential d.succ where val := fun x μ => match μ with | Sum.inl 0 => 0 | Sum.inr 0 => 0 | Sum.inr ⟨Nat.succ i, h⟩ => -E₀ ⟨i, Nat.succ_lt_succ_i...
Source project: Physlib
Person-level attribution pending.
Electromagnetism.ElectromagneticPotential.harmonicWaveX_isExtrema
Project documentation
The electromagnetic potential for a Harmonic wave travelling in the x-direction with wave number k. -/ noncomputable def harmonicWaveX (𝓕 : FreeSpace) (k : ℝ) (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) : ElectromagneticPotential d.succ where val := fun x μ => match μ with | Sum.inl 0 => 0 | Sum.inr 0 => 0 | Sum.inr ⟨Nat.succ i, h⟩ => -E₀ ⟨i, Nat.succ_lt_succ_i...
Source project: Physlib
Person-level attribution pending.
Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave
Project documentation
The electromagnetic potential for a Harmonic wave travelling in the x-direction with wave number k. -/ noncomputable def harmonicWaveX (𝓕 : FreeSpace) (k : ℝ) (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) : ElectromagneticPotential d.succ where val := fun x μ => match μ with | Sum.inl 0 => 0 | Sum.inr 0 => 0 | Sum.inr ⟨Nat.succ i, h⟩ => -E₀ ⟨i, Nat.succ_lt_succ_i...
Source project: Physlib
Person-level attribution pending.
Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_space_deriv_succ
Project documentation
The electromagnetic potential for a Harmonic wave travelling in the x-direction with wave number k. -/ noncomputable def harmonicWaveX (𝓕 : FreeSpace) (k : ℝ) (E₀ : Fin d → ℝ) (φ : Fin d → ℝ) : ElectromagneticPotential d.succ where val := fun x μ => match μ with | Sum.inl 0 => 0 | Sum.inr 0 => 0 | Sum.inr ⟨Nat.succ i, h⟩ => -E₀ ⟨i, Nat.succ_lt_succ_i...
Source project: Physlib
Person-level attribution pending.