← Mathematical handbook

Conditional moments from independent uniform sampling

theorem Verification.quadraticSample_second_uniform (b : ℝ) (hb : 0 ≤ b) : MeasureTheory.Measure.map (fun (p : ↑unitInterval × ↑unitInterval) => quadraticSample b p 1) MeasureTheory.volume = MeasureTheory.volume

noncomputable def Verification.quadraticMoment (b : ℝ) (w : ↑unitInterval → ℝ) (k : ℕ) (a : ℝ) : ℝ

Equations

• Verification.quadraticMoment b w k a = ∫ (t : ↑unitInterval), w t * Verification.unitClamp (a + b * (1 - ↑t) ^ 2) ^ k

theorem Verification.continuous_quadraticMoment (b : ℝ) (w : ↑unitInterval → ℝ) (hw : Continuous w) (k : ℕ) : Continuous (quadraticMoment b w k)

theorem Verification.quadratic_kernel_moment_sample (b : ℝ) (hb : 0 ≤ b) (w : ↑unitInterval → ℝ) (hw : Continuous w) (k : ℕ) : ∫ (v : ↑unitInterval) (t : ↑unitInterval), w t * quadraticKernel b hb v t ^ k = ∫ (u : ↑unitInterval) (t : ↑unitInterval) (z : ↑unitInterval), w t * unitClamp (↑z + b * ((1 - ↑t) ^ 2 - (1 - ↑u) ^ 2)) ^ k