Documentation
Verification
.
ClampNoiseMoments
Search
return to top
source
Imports
Init
Verification.ClampedRhoOptimization
Verification.RampIntegrals
Imported by
Verification
.
clamp_noise_sub
Verification
.
clamp_noise_sub_sq
Verification
.
clamp_noise_add
Verification
.
clamp_noise_add_sq
Verification
.
clamp_noise_moment
Verification
.
clamp_noise_square_pair
← Mathematical handbook
Uniform-noise moments of a translated clamp
#
source
theorem
Verification
.
clamp_noise_sub
(
h
:
↑
unitInterval
)
:
∫
(
z
:
↑
unitInterval
)
,
unitClamp
(
↑
z
-
↑
h
)
=
(
1
-
↑
h
)
^
2
/
2
source
theorem
Verification
.
clamp_noise_sub_sq
(
h
:
↑
unitInterval
)
:
∫
(
z
:
↑
unitInterval
)
,
unitClamp
(
↑
z
-
↑
h
)
^
2
=
(
1
-
↑
h
)
^
3
/
3
source
theorem
Verification
.
clamp_noise_add
(
h
:
↑
unitInterval
)
:
∫
(
z
:
↑
unitInterval
)
,
unitClamp
(
↑
z
+
↑
h
)
=
1
-
(
1
-
↑
h
)
^
2
/
2
source
theorem
Verification
.
clamp_noise_add_sq
(
h
:
↑
unitInterval
)
:
∫
(
z
:
↑
unitInterval
)
,
unitClamp
(
↑
z
+
↑
h
)
^
2
=
1
-
(
1
-
↑
h
)
^
2
+
(
1
-
↑
h
)
^
3
/
3
source
theorem
Verification
.
clamp_noise_moment
(
d
:
ℝ
)
(
hd
:
|
d
|
≤
1
)
:
∫
(
z
:
↑
unitInterval
)
,
unitClamp
(
↑
z
+
d
)
=
1
/
2
+
d
-
d
*
|
d
|
/
2
source
theorem
Verification
.
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