← Mathematical handbook

Polynomial coefficient integrals for slopes between zero and one

noncomputable def Verification.noiseMoment (k : ℕ) (d : ℝ) : ℝ

Equations

• Verification.noiseMoment k d = ∫ (z : ↑unitInterval), Verification.unitClamp (↑z + d) ^ k

theorem Verification.continuous_noiseMoment (k : ℕ) : Continuous (noiseMoment k)

theorem Verification.quadratic_kernel_moment_pair (b : ℝ) (hb : 0 ≤ b) (w : ↑unitInterval → ℝ) (hw : Continuous w) (k : ℕ) : ∫ (v : ↑unitInterval) (t : ↑unitInterval), w t * quadraticKernel b hb v t ^ k = ∫ (p : ↑unitInterval × ↑unitInterval), w p.2 * noiseMoment k (b * squareDelta p)

theorem Verification.quadraticBand_xi_noise (b : ℝ) (hb : 0 ≤ b) : (quadraticBand b hb).chatterjeeXi = (6 * ∫ (p : ↑unitInterval × ↑unitInterval), noiseMoment 2 (b * squareDelta p)) - 2

theorem Verification.integral_noise_square (b : ℝ) (hb : b ∈ Set.Icc 0 1) : ∫ (p : ↑unitInterval × ↑unitInterval), noiseMoment 2 (b * squareDelta p) = 1 / 3 + 4 * b ^ 2 / 45 - 4 * b ^ 3 / 105

theorem Verification.quadraticBand_xi_polynomial (b : ℝ) (hb : b ∈ Set.Icc 0 1) : (quadraticBand b ⋯).chatterjeeXi = 8 * b ^ 2 * (7 - 3 * b) / 105

theorem Verification.integral_noise_weighted (b : ℝ) (hb : b ∈ Set.Icc 0 1) : ∫ (p : ↑unitInterval × ↑unitInterval), squarePotential p.2 * noiseMoment 1 (b * squareDelta p) = 1 / 6 + 4 * b / 45 - b ^ 2 / 35