Documentation

Copula.Rank.Region.XiBlest.Support.ClampNoiseMoments

← Copula mathematical handbook

Uniform-noise moments of a translated clamp #

source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clamp_noise_sub (h : ↑unitInterval) :
∫ (z : ↑unitInterval), unitClamp (↑z - ↑h) = (1 - ↑h) ^ 2 / 2
source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clamp_noise_sub_sq (h : ↑unitInterval) :
∫ (z : ↑unitInterval), unitClamp (↑z - ↑h) ^ 2 = (1 - ↑h) ^ 3 / 3
source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clamp_noise_add (h : ↑unitInterval) :
∫ (z : ↑unitInterval), unitClamp (↑z + ↑h) = 1 - (1 - ↑h) ^ 2 / 2
source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clamp_noise_add_sq (h : ↑unitInterval) :
∫ (z : ↑unitInterval), unitClamp (↑z + ↑h) ^ 2 = 1 - (1 - ↑h) ^ 2 + (1 - ↑h) ^ 3 / 3
source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clamp_noise_moment (d : ℝ) (hd : |d| ≤ 1) :
∫ (z : ↑unitInterval), unitClamp (↑z + d) = 1 / 2 + d - d * |d| / 2
source
theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.clamp_noise_square_pair (d : ℝ) (hd : |d| ≤ 1) :
((∫ (z : ↑unitInterval), unitClamp (↑z + d) ^ 2) + ∫ (z : ↑unitInterval), unitClamp (↑z - d) ^ 2) / 2 = 1 / 3 + d ^ 2 / 2 - |d| ^ 3 / 3