← Mathematical handbook

noncomputable def Verification.debyeKernel (x : ℝ) : ℝ

Equations

• Verification.debyeKernel x = (dslope Real.exp 0 x)⁻¹

theorem Verification.continuous_debyeKernel : Continuous debyeKernel

theorem Verification.debyeKernel_of_ne {x : ℝ} (hx : x ≠ 0) : debyeKernel x = x / (Real.exp x - 1)

theorem Verification.integrable_debye_section {θ : ℝ} (hθ : θ ≠ 0) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ↑v / (Real.exp (θ * ↑v) - 1)) MeasureTheory.volume

noncomputable def Verification.debyeOne (θ : ℝ) : ℝ

The first Debye function on nonzero arguments, as normalized in Table 6.

Equations

• Verification.debyeOne θ = 1 / θ * ∫ (t : ℝ) in 0..θ, t / (Real.exp t - 1)

theorem Verification.integral_debye_section {θ : ℝ} (hθ : θ ≠ 0) : ∫ (v : ↑unitInterval), ↑v / (Real.exp (θ * ↑v) - 1) = debyeOne θ / θ

noncomputable def Verification.debyeTwo (θ : ℝ) : ℝ

The second Debye function on nonzero arguments, with the Table 6 normalization.

Equations

• Verification.debyeTwo θ = 2 / θ ^ 2 * ∫ (t : ℝ) in 0..θ, t ^ 2 / (Real.exp t - 1)

theorem Verification.integrable_debye_second_section {θ : ℝ} (hθ : θ ≠ 0) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ↑v ^ 2 / (Real.exp (θ * ↑v) - 1)) MeasureTheory.volume

theorem Verification.integral_debye_second_section {θ : ℝ} (hθ : θ ≠ 0) : ∫ (v : ↑unitInterval), ↑v ^ 2 / (Real.exp (θ * ↑v) - 1) = debyeTwo θ / (2 * θ)

theorem Verification.debyeKernel_neg (x : ℝ) : debyeKernel (-x) = debyeKernel x + x

theorem Verification.debyeOne_kernel_integral {θ : ℝ} (hθ : θ ≠ 0) : debyeOne θ = ∫ (v : ↑unitInterval), debyeKernel (θ * ↑v)

theorem Verification.debyeTwo_kernel_integral {θ : ℝ} (hθ : θ ≠ 0) : debyeTwo θ = ∫ (v : ↑unitInterval), 2 * ↑v * debyeKernel (θ * ↑v)

theorem Verification.debyeOne_neg {θ : ℝ} (hθ : θ ≠ 0) : debyeOne (-θ) = debyeOne θ + θ / 2

theorem Verification.debyeTwo_neg {θ : ℝ} (hθ : θ ≠ 0) : debyeTwo (-θ) = debyeTwo θ + 2 * θ / 3