:: RANDOM_2 semantic presentation

REAL is non empty non trivial non finite V139() V140() V141() V145() set
NAT is non empty non trivial V17() V18() V19() non finite cardinal limit_cardinal V139() V140() V141() V142() V143() V144() V145() Element of bool REAL
bool REAL is non empty non trivial non finite set
ExtREAL is non empty V140() set
[:NAT,ExtREAL:] is Relation-like non empty non trivial non finite V147() set
bool [:NAT,ExtREAL:] is non empty non trivial non finite set
bool ExtREAL is non empty set
NAT is non empty non trivial V17() V18() V19() non finite cardinal limit_cardinal V139() V140() V141() V142() V143() V144() V145() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V139() V145() set
RAT is non empty non trivial non finite V139() V140() V141() V142() V145() set
INT is non empty non trivial non finite V139() V140() V141() V142() V143() V145() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V18() V19() V21() V22() V23() ext-real non positive non negative finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V38() V39() V139() V140() V141() V142() V143() V144() V145() V146() V147() V148() V149() set
1 is non empty V17() V18() V19() V23() ext-real positive non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
{{},1} is non empty finite V31() V139() V140() V141() V142() V143() V144() set
[:NAT,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:REAL,REAL:] is non empty non trivial non finite set
bool RAT is non empty non trivial non finite set
K435(NAT) is V187() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V146() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V146() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V146() V147() V148() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V146() V147() V148() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K721() is set
2 is non empty V17() V18() V19() V23() ext-real positive non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
1 -tuples_on NAT is FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b₁ = 1 } is set
3 is non empty V17() V18() V19() V23() ext-real positive non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V18() V19() V21() V22() V23() ext-real non positive non negative finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V38() V39() V104() V139() V140() V141() V142() V143() V144() V145() V146() V147() V148() V149() V161() Element of NAT
- 1 is non empty ext-real non positive negative V38() V39() Element of REAL
K473() is non empty ext-real non positive negative V39() Element of ExtREAL
K472() is non empty ext-real positive non negative V39() Element of ExtREAL
+infty is non empty ext-real positive non negative V39() set
-infty is non empty ext-real non positive negative V39() set
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() V222( REAL ) V223( REAL ) V247( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
Seg 1 is non empty trivial finite 1 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial finite V31() 1 -element V139() V140() V141() V142() V143() V144() set
Seg 2 is non empty finite 2 -element V139() V140() V141() V142() V143() V144() Element of bool NAT
{ b₁ where b₁ is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty finite V31() V139() V140() V141() V142() V143() V144() set
Omega is Relation-like Function-like one-to-one set
dom Omega is set
bool (dom Omega) is non empty set
Sigma is Element of bool (dom Omega)
v is Element of bool (dom Omega)
Omega | Sigma is Relation-like Function-like set
rng (Omega | Sigma) is set
Omega | v is Relation-like Function-like set
rng (Omega | v) is set
v1 is set
dom (Omega | Sigma) is set
g is set
(Omega | Sigma) . g is set
dom (Omega | v) is set
u is set
(Omega | v) . u is set
Omega . g is set
Omega . u is set
Sigma /\ v is Element of bool (dom Omega)
Sigma is Relation-like Function-like set
Omega is Relation-like Function-like set
Sigma (#) Omega is Relation-like Function-like set
rng (Sigma (#) Omega) is set
rng Sigma is set
Omega | (rng Sigma) is Relation-like Function-like set
rng (Omega | (rng Sigma)) is set
v is set
dom (Sigma (#) Omega) is set
v1 is set
(Sigma (#) Omega) . v1 is set
dom Sigma is set
Sigma . v1 is set
dom Omega is set
g is set
Omega . g is set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v1 is set
abs the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
dom (abs the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma) is non empty Element of bool Omega
(abs the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma) . v1 is ext-real V38() V39() Element of REAL
the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma . v1 is ext-real V38() V39() Element of REAL
abs ( the Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma . v1) is ext-real V38() V39() Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
v is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
abs v is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v1 is set
dom (abs v) is non empty Element of bool Omega
(abs v) . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
abs (v . v1) is ext-real V38() V39() Element of REAL
Omega is non empty set
Omega --> 1 is Relation-like Omega -defined NAT -valued RAT -valued INT -valued Function-like non empty total quasi_total V146() V147() V148() V149() Element of bool [:Omega,NAT:]
[:Omega,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:Omega,NAT:] is non empty non trivial non finite set
chi (Omega,Omega) is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is Relation-like non empty V147() set
bool [:Omega,ExtREAL:] is non empty set
dom (chi (Omega,Omega)) is Element of bool Omega
bool Omega is non empty set
dom (Omega --> 1) is non empty Element of bool Omega
v is set
(chi (Omega,Omega)) . v is ext-real Element of ExtREAL
(Omega --> 1) . v is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V161() Element of REAL
(chi (Omega,Omega)) . v is ext-real Element of ExtREAL
(Omega --> 1) . v is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V161() Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is ext-real V38() V39() Element of REAL
Omega --> Sigma is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
v is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
Omega --> 1 is Relation-like Omega -defined NAT -valued RAT -valued INT -valued Function-like non empty total quasi_total V146() V147() V148() V149() Element of bool [:Omega,NAT:]
[:Omega,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:Omega,NAT:] is non empty non trivial non finite set
dom (Omega --> 1) is non empty Element of bool Omega
rng (Omega --> 1) is non empty V139() V140() V141() V142() V143() V144() Element of bool REAL
u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
R_EAL u1 is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is Relation-like non empty V147() set
bool [:Omega,ExtREAL:] is non empty set
u is Element of v
chi (u,Omega) is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
dom (Omega --> Sigma) is non empty Element of bool Omega
dom u1 is non empty Element of bool Omega
h is set
(Omega --> Sigma) . h is ext-real V38() V39() Element of REAL
Sigma * 1 is ext-real V38() V39() Element of REAL
u1 . h is ext-real V38() V39() Element of REAL
Sigma * (u1 . h) is ext-real V38() V39() Element of REAL
Sigma (#) u1 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Omega is non empty set
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) Sigma is Relation-like Function-like set
(- Sigma) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
abs Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(abs Sigma) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (- Sigma) is Element of bool Omega
bool Omega is non empty set
dom Sigma is Element of bool Omega
dom ((- Sigma) to_power 2) is Element of bool Omega
dom (Sigma to_power 2) is Element of bool Omega
dom (abs Sigma) is Element of bool Omega
dom ((abs Sigma) to_power 2) is Element of bool Omega
v is Element of Omega
(Sigma to_power 2) . v is ext-real V38() V39() Element of REAL
((- Sigma) to_power 2) . v is ext-real V38() V39() Element of REAL
((abs Sigma) to_power 2) . v is ext-real V38() V39() Element of REAL
(- Sigma) . v is ext-real V38() V39() Element of REAL
((- Sigma) . v) to_power 2 is ext-real V38() V39() Element of REAL
Sigma . v is ext-real V38() V39() Element of REAL
- (Sigma . v) is ext-real V38() V39() Element of REAL
(- (Sigma . v)) to_power 2 is ext-real V38() V39() Element of REAL
(Sigma . v) to_power 2 is ext-real V38() V39() Element of REAL
(abs Sigma) . v is ext-real V38() V39() Element of REAL
((abs Sigma) . v) to_power 2 is ext-real V38() V39() Element of REAL
abs (Sigma . v) is ext-real V38() V39() Element of REAL
(abs (Sigma . v)) to_power 2 is ext-real V38() V39() Element of REAL
v is Element of Omega
(Sigma to_power 2) . v is ext-real V38() V39() Element of REAL
((- Sigma) to_power 2) . v is ext-real V38() V39() Element of REAL
v1 is Element of Omega
(Sigma to_power 2) . v1 is ext-real V38() V39() Element of REAL
((abs Sigma) to_power 2) . v1 is ext-real V38() V39() Element of REAL
Omega is non empty set
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
Sigma is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma + v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(Sigma + v) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma (#) v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
2 (#) (Sigma (#) v) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(Sigma to_power 2) + (2 (#) (Sigma (#) v)) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
v to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Sigma - v is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- v is Relation-like Function-like V146() set
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) v is Relation-like Function-like set
Sigma + (- v) is Relation-like Function-like set
(Sigma - v) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(Sigma to_power 2) - (2 (#) (Sigma (#) v)) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- (2 (#) (Sigma (#) v)) is Relation-like Function-like V146() set
K105(1) (#) (2 (#) (Sigma (#) v)) is Relation-like Function-like set
(Sigma to_power 2) + (- (2 (#) (Sigma (#) v))) is Relation-like Function-like set
((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (Sigma to_power 2) is Element of bool Omega
bool Omega is non empty set
dom Sigma is Element of bool Omega
v1 is Element of Omega
(Sigma to_power 2) . v1 is ext-real V38() V39() Element of REAL
Sigma . v1 is ext-real V38() V39() Element of REAL
(Sigma . v1) to_power 2 is ext-real V38() V39() Element of REAL
dom (v to_power 2) is Element of bool Omega
dom v is Element of bool Omega
v1 is Element of Omega
(v to_power 2) . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
(v . v1) to_power 2 is ext-real V38() V39() Element of REAL
dom (2 (#) (Sigma (#) v)) is Element of bool Omega
dom (Sigma (#) v) is Element of bool Omega
(dom Sigma) /\ (dom v) is Element of bool Omega
v1 is Element of Omega
(2 (#) (Sigma (#) v)) . v1 is ext-real V38() V39() Element of REAL
(Sigma (#) v) . v1 is ext-real V38() V39() Element of REAL
2 * ((Sigma (#) v) . v1) is ext-real V38() V39() Element of REAL
Sigma . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
(Sigma . v1) * (v . v1) is ext-real V38() V39() Element of REAL
2 * ((Sigma . v1) * (v . v1)) is ext-real V38() V39() Element of REAL
2 * (Sigma . v1) is ext-real V38() V39() Element of REAL
(2 * (Sigma . v1)) * (v . v1) is ext-real V38() V39() Element of REAL
dom ((Sigma + v) to_power 2) is Element of bool Omega
dom (Sigma + v) is Element of bool Omega
dom ((Sigma - v) to_power 2) is Element of bool Omega
dom (Sigma - v) is Element of bool Omega
dom ((Sigma to_power 2) + (2 (#) (Sigma (#) v))) is Element of bool Omega
(dom Sigma) /\ (dom (2 (#) (Sigma (#) v))) is Element of bool Omega
dom ((Sigma to_power 2) - (2 (#) (Sigma (#) v))) is Element of bool Omega
dom (((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2)) is Element of bool Omega
(dom ((Sigma to_power 2) + (2 (#) (Sigma (#) v)))) /\ (dom v) is Element of bool Omega
((dom Sigma) /\ (dom (2 (#) (Sigma (#) v)))) /\ (dom v) is Element of bool Omega
((dom Sigma) /\ (dom v)) /\ (dom v) is Element of bool Omega
dom (((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2)) is Element of bool Omega
(dom ((Sigma to_power 2) - (2 (#) (Sigma (#) v)))) /\ (dom v) is Element of bool Omega
v1 is Element of Omega
((Sigma + v) to_power 2) . v1 is ext-real V38() V39() Element of REAL
(Sigma + v) . v1 is ext-real V38() V39() Element of REAL
((Sigma + v) . v1) to_power 2 is ext-real V38() V39() Element of REAL
Sigma . v1 is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
(Sigma . v1) + (v . v1) is ext-real V38() V39() Element of REAL
((Sigma . v1) + (v . v1)) to_power 2 is ext-real V38() V39() Element of REAL
((Sigma . v1) + (v . v1)) ^2 is ext-real V38() V39() Element of REAL
K104(((Sigma . v1) + (v . v1)),((Sigma . v1) + (v . v1))) is ext-real V38() V39() set
(Sigma . v1) ^2 is ext-real V38() V39() Element of REAL
K104((Sigma . v1),(Sigma . v1)) is ext-real V38() V39() set
2 * (Sigma . v1) is ext-real V38() V39() Element of REAL
(2 * (Sigma . v1)) * (v . v1) is ext-real V38() V39() Element of REAL
((Sigma . v1) ^2) + ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(v . v1) ^2 is ext-real V38() V39() Element of REAL
K104((v . v1),(v . v1)) is ext-real V38() V39() set
(((Sigma . v1) ^2) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
(Sigma . v1) to_power 2 is ext-real V38() V39() Element of REAL
((Sigma . v1) to_power 2) + ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
(v . v1) to_power 2 is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
(Sigma to_power 2) . v1 is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) + ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) + ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
(v to_power 2) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) + ((2 * (Sigma . v1)) * (v . v1))) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
(2 (#) (Sigma (#) v)) . v1 is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) + ((2 (#) (Sigma (#) v)) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) + ((2 (#) (Sigma (#) v)) . v1)) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) + (2 (#) (Sigma (#) v))) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) + (2 (#) (Sigma (#) v))) . v1) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2)) . v1 is ext-real V38() V39() Element of REAL
((Sigma - v) to_power 2) . v1 is ext-real V38() V39() Element of REAL
(Sigma - v) . v1 is ext-real V38() V39() Element of REAL
((Sigma - v) . v1) to_power 2 is ext-real V38() V39() Element of REAL
(Sigma . v1) - (v . v1) is ext-real V38() V39() Element of REAL
((Sigma . v1) - (v . v1)) to_power 2 is ext-real V38() V39() Element of REAL
((Sigma . v1) - (v . v1)) ^2 is ext-real V38() V39() Element of REAL
K104(((Sigma . v1) - (v . v1)),((Sigma . v1) - (v . v1))) is ext-real V38() V39() set
((Sigma . v1) ^2) - ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma . v1) ^2) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
((Sigma . v1) to_power 2) - ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) ^2) is ext-real V38() V39() Element of REAL
(((Sigma . v1) to_power 2) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) - ((2 * (Sigma . v1)) * (v . v1)) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) - ((2 * (Sigma . v1)) * (v . v1))) + ((v . v1) to_power 2) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) - ((2 * (Sigma . v1)) * (v . v1))) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) . v1) - ((2 (#) (Sigma (#) v)) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) . v1) - ((2 (#) (Sigma (#) v)) . v1)) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
((Sigma to_power 2) - (2 (#) (Sigma (#) v))) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) - (2 (#) (Sigma (#) v))) . v1) + ((v to_power 2) . v1) is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2)) . v1 is ext-real V38() V39() Element of REAL
v1 is Element of Omega
((Sigma + v) to_power 2) . v1 is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) + (2 (#) (Sigma (#) v))) + (v to_power 2)) . v1 is ext-real V38() V39() Element of REAL
g is Element of Omega
((Sigma - v) to_power 2) . g is ext-real V38() V39() Element of REAL
(((Sigma to_power 2) - (2 (#) (Sigma (#) v))) + (v to_power 2)) . g is ext-real V38() V39() Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v is Relation-like Sigma -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Probability of Sigma
P2M v is Relation-like Sigma -defined ExtREAL -valued Function-like non empty total quasi_total V147() V155() nonnegative V204(Omega,Sigma) Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is Relation-like non empty V147() set
bool [:Sigma,ExtREAL:] is non empty set
abs v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(abs v1) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
expect (v1,v) is ext-real V38() V39() Element of REAL
Omega --> (expect (v1,v)) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
g is Element of Sigma
(P2M v) . g is ext-real Element of ExtREAL
Omega --> 1 is Relation-like Omega -defined NAT -valued RAT -valued INT -valued Function-like non empty total quasi_total V146() V147() V148() V149() Element of bool [:Omega,NAT:]
[:Omega,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V146() V147() V148() V149() set
bool [:Omega,NAT:] is non empty non trivial non finite set
dom (Omega --> 1) is non empty Element of bool Omega
rng (Omega --> 1) is non empty V139() V140() V141() V142() V143() V144() Element of bool REAL
y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
R_EAL y is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
[:Omega,ExtREAL:] is Relation-like non empty V147() set
bool [:Omega,ExtREAL:] is non empty set
chi (g,Omega) is Relation-like Omega -defined ExtREAL -valued Function-like V147() Element of bool [:Omega,ExtREAL:]
dom (Omega --> (expect (v1,v))) is non empty Element of bool Omega
dom y is non empty Element of bool Omega
y is set
(Omega --> (expect (v1,v))) . y is ext-real V38() V39() Element of REAL
(expect (v1,v)) * 1 is ext-real V38() V39() Element of REAL
y . y is ext-real V38() V39() Element of REAL
(expect (v1,v)) * (y . y) is ext-real V38() V39() Element of REAL
(expect (v1,v)) (#) y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v1 - y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- y is Relation-like Function-like V146() set
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) y is Relation-like Function-like set
v1 + (- y) is Relation-like Function-like set
- 1 is non empty ext-real non positive negative V38() V39() V104() V161() Element of INT
(- 1) (#) ((expect (v1,v)) (#) y) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Y1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
2 * (expect (v1,v)) is ext-real V38() V39() Element of REAL
(2 * (expect (v1,v))) (#) v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
(- 1) (#) ((2 * (expect (v1,v))) (#) v1) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((abs v1) to_power 2) - ((2 * (expect (v1,v))) (#) v1) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- ((2 * (expect (v1,v))) (#) v1) is Relation-like Function-like V146() set
K105(1) (#) ((2 * (expect (v1,v))) (#) v1) is Relation-like Function-like set
((abs v1) to_power 2) + (- ((2 * (expect (v1,v))) (#) v1)) is Relation-like Function-like set
v1 to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((expect (v1,v)) (#) y) (#) v1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
2 (#) (((expect (v1,v)) (#) y) (#) v1) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
(v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is Relation-like Function-like V146() set
K105(1) (#) (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is Relation-like Function-like set
(v1 to_power 2) + (- (2 (#) (((expect (v1,v)) (#) y) (#) v1))) is Relation-like Function-like set
((expect (v1,v)) (#) y) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) + (((expect (v1,v)) (#) y) to_power 2) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(v1 to_power 2) + (- ((2 * (expect (v1,v))) (#) v1)) is Relation-like Function-like set
(expect (v1,v)) * (expect (v1,v)) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (expect (v1,v))) (#) y is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (v1 to_power 2) is Element of bool Omega
dom v1 is non empty Element of bool Omega
dom (2 (#) (((expect (v1,v)) (#) y) (#) v1)) is non empty Element of bool Omega
dom (((expect (v1,v)) (#) y) (#) v1) is non empty Element of bool Omega
dom ((expect (v1,v)) (#) y) is non empty Element of bool Omega
(dom ((expect (v1,v)) (#) y)) /\ (dom v1) is Element of bool Omega
Omega /\ (dom v1) is Element of bool Omega
dom (((expect (v1,v)) (#) y) to_power 2) is Element of bool Omega
dom (((expect (v1,v)) * (expect (v1,v))) (#) y) is non empty Element of bool Omega
dom ((2 * (expect (v1,v))) (#) v1) is non empty Element of bool Omega
dom ((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) is Element of bool Omega
(dom v1) /\ (Omega /\ (dom v1)) is Element of bool Omega
(dom v1) /\ (dom v1) is Element of bool Omega
((dom v1) /\ (dom v1)) /\ Omega is Element of bool Omega
(dom v1) /\ Omega is Element of bool Omega
dom ((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) is Element of bool Omega
(dom (v1 to_power 2)) /\ (dom ((2 * (expect (v1,v))) (#) v1)) is Element of bool Omega
dom (((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) + (((expect (v1,v)) (#) y) to_power 2)) is Element of bool Omega
(dom ((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1)))) /\ (dom (((expect (v1,v)) (#) y) to_power 2)) is Element of bool Omega
Omega /\ Omega is set
(dom v1) /\ (Omega /\ Omega) is Element of bool Omega
dom (((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y)) is Element of bool Omega
f2 is Element of Omega
(((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) + (((expect (v1,v)) (#) y) to_power 2)) . f2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y)) . f2 is ext-real V38() V39() Element of REAL
((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) . f2 is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) to_power 2) . f2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) - (2 (#) (((expect (v1,v)) (#) y) (#) v1))) . f2) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
(v1 to_power 2) . f2 is ext-real V38() V39() Element of REAL
(2 (#) (((expect (v1,v)) (#) y) (#) v1)) . f2 is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - ((2 (#) (((expect (v1,v)) (#) y) (#) v1)) . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 (#) (((expect (v1,v)) (#) y) (#) v1)) . f2)) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) (#) v1) . f2 is ext-real V38() V39() Element of REAL
2 * ((((expect (v1,v)) (#) y) (#) v1) . f2) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) (#) v1) . f2)) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) (#) v1) . f2))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) (#) y) . f2 is ext-real V38() V39() Element of REAL
v1 . f2 is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) . f2) * (v1 . f2) is ext-real V38() V39() Element of REAL
2 * ((((expect (v1,v)) (#) y) . f2) * (v1 . f2)) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) . f2) * (v1 . f2))) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * ((((expect (v1,v)) (#) y) . f2) * (v1 . f2)))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
y . f2 is ext-real V38() V39() Element of REAL
(expect (v1,v)) * (y . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (y . f2)) * (v1 . f2) is ext-real V38() V39() Element of REAL
2 * (((expect (v1,v)) * (y . f2)) * (v1 . f2)) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * (y . f2)) * (v1 . f2))) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * (y . f2)) * (v1 . f2)))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * 1) * (v1 . f2) is ext-real V38() V39() Element of REAL
2 * (((expect (v1,v)) * 1) * (v1 . f2)) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * 1) * (v1 . f2))) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (2 * (((expect (v1,v)) * 1) * (v1 . f2)))) + ((((expect (v1,v)) (#) y) to_power 2) . f2) is ext-real V38() V39() Element of REAL
(2 * (expect (v1,v))) * (v1 . f2) is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2)) is ext-real V38() V39() Element of REAL
(((expect (v1,v)) (#) y) . f2) to_power 2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((((expect (v1,v)) (#) y) . f2) to_power 2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (y . f2)) to_power 2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * (y . f2)) to_power 2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * 1) to_power 2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * 1) to_power 2) is ext-real V38() V39() Element of REAL
(expect (v1,v)) ^2 is ext-real V38() V39() Element of REAL
K104((expect (v1,v)),(expect (v1,v))) is ext-real V38() V39() set
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((expect (v1,v)) ^2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((expect (v1,v)) * (expect (v1,v))) is ext-real V38() V39() Element of REAL
((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) . f2 is ext-real V38() V39() Element of REAL
(((expect (v1,v)) * (expect (v1,v))) (#) y) . f2 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) - ((2 * (expect (v1,v))) (#) v1)) . f2) + ((((expect (v1,v)) * (expect (v1,v))) (#) y) . f2) is ext-real V38() V39() Element of REAL
((2 * (expect (v1,v))) (#) v1) . f2 is ext-real V38() V39() Element of REAL
((v1 to_power 2) . f2) - (((2 * (expect (v1,v))) (#) v1) . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - (((2 * (expect (v1,v))) (#) v1) . f2)) + ((((expect (v1,v)) * (expect (v1,v))) (#) y) . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + ((((expect (v1,v)) * (expect (v1,v))) (#) y) . f2) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (expect (v1,v))) * (y . f2) is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * (expect (v1,v))) * (y . f2)) is ext-real V38() V39() Element of REAL
((expect (v1,v)) * (expect (v1,v))) * 1 is ext-real V38() V39() Element of REAL
(((v1 to_power 2) . f2) - ((2 * (expect (v1,v))) * (v1 . f2))) + (((expect (v1,v)) * (expect (v1,v))) * 1) is ext-real V38() V39() Element of REAL
abs Y1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(abs Y1) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
v1 - ((expect (v1,v)) (#) y) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- ((expect (v1,v)) (#) y) is Relation-like Function-like V146() set
K105(1) (#) ((expect (v1,v)) (#) y) is Relation-like Function-like set
v1 + (- ((expect (v1,v)) (#) y)) is Relation-like Function-like set
(v1 - ((expect (v1,v)) (#) y)) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
(((abs v1) to_power 2) - ((2 * (expect (v1,v))) (#) v1)) + (((expect (v1,v)) * (expect (v1,v))) (#) y) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
Integral ((P2M v),((abs Y1) to_power 2)) is ext-real Element of ExtREAL
Y2 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
s2 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v1 - Y2 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- Y2 is Relation-like Function-like V146() set
K105(1) (#) Y2 is Relation-like Function-like set
v1 + (- Y2) is Relation-like Function-like set
abs s2 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(abs s2) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
f2 is ext-real V38() V39() Element of REAL
Integral ((P2M v),((abs s2) to_power 2)) is ext-real Element of ExtREAL
x is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
Y3 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
v1 - x is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- x is Relation-like Function-like V146() set
K105(1) (#) x is Relation-like Function-like set
v1 + (- x) is Relation-like Function-like set
abs Y3 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(abs Y3) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
G2 is ext-real V38() V39() Element of REAL
Integral ((P2M v),((abs Y3) to_power 2)) is ext-real Element of ExtREAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
v is Relation-like Sigma -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Probability of Sigma
P2M v is Relation-like Sigma -defined ExtREAL -valued Function-like non empty total quasi_total V147() V155() nonnegative V204(Omega,Sigma) Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is Relation-like non empty V147() set
bool [:Sigma,ExtREAL:] is non empty set
v1 is ext-real V38() V39() Element of REAL
v1 to_power 2 is ext-real V38() V39() Element of REAL
g is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
abs g is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(abs g) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
expect (g,v) is ext-real V38() V39() Element of REAL
{ b₁ where b₁ is Element of Omega : v1 <= |.((g . b₁) - (expect (g,v))).| } is set
v . { b₁ where b₁ is Element of Omega : v1 <= |.((g . b₁) - (expect (g,v))).| } is ext-real V38() V39() Element of REAL
(Omega,Sigma,v,g) is ext-real V38() V39() Element of REAL
(Omega,Sigma,v,g) / (v1 to_power 2) is ext-real V38() V39() Element of REAL
{ b₁ where b₁ is Element of Omega : v1 to_power 2 <= (abs ((g . b₁) - (expect (g,v)))) to_power 2 } is set
u is set
v1 ^2 is ext-real V38() V39() Element of REAL
K104(v1,v1) is ext-real V38() V39() set
g . u is ext-real V38() V39() Element of REAL
(g . u) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . u) - (expect (g,v)))) ^2 is ext-real V38() V39() Element of REAL
K104((abs ((g . u) - (expect (g,v)))),(abs ((g . u) - (expect (g,v))))) is ext-real V38() V39() set
(abs ((g . u) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
|.((g . u1) - (expect (g,v))).| is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
|.((g . u1) - (expect (g,v))).| is ext-real V38() V39() Element of REAL
u is set
g . u is ext-real V38() V39() Element of REAL
(g . u) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u) - (expect (g,v))) is ext-real V38() V39() Element of REAL
v1 ^2 is ext-real V38() V39() Element of REAL
K104(v1,v1) is ext-real V38() V39() set
(abs ((g . u) - (expect (g,v)))) ^2 is ext-real V38() V39() Element of REAL
K104((abs ((g . u) - (expect (g,v)))),(abs ((g . u) - (expect (g,v))))) is ext-real V38() V39() set
(abs ((g . u) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u1) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . u1) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
u1 is Element of Omega
g . u1 is ext-real V38() V39() Element of REAL
(g . u1) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . u1) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . u1) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
Omega --> (expect (g,v)) is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
u is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
g - u1 is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
- u1 is Relation-like Function-like V146() set
K105(1) is non empty ext-real non positive negative V38() V39() set
K105(1) (#) u1 is Relation-like Function-like set
g + (- u1) is Relation-like Function-like set
abs u is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative Real-Valued-Random-Variable of Sigma
(abs u) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() nonnegative Element of bool [:Omega,REAL:]
Integral ((P2M v),((abs u) to_power 2)) is ext-real Element of ExtREAL
h is Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Real-Valued-Random-Variable of Sigma
{ b₁ where b₁ is Element of Omega : v1 to_power 2 <= h . b₁ } is set
v . { b₁ where b₁ is Element of Omega : v1 to_power 2 <= h . b₁ } is ext-real V38() V39() Element of REAL
expect (h,v) is ext-real V38() V39() Element of REAL
(expect (h,v)) / (v1 to_power 2) is ext-real V38() V39() Element of REAL
dom g is non empty Element of bool Omega
dom (Omega --> (expect (g,v))) is non empty Element of bool Omega
g - (Omega --> (expect (g,v))) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
- (Omega --> (expect (g,v))) is Relation-like Function-like V146() set
K105(1) (#) (Omega --> (expect (g,v))) is Relation-like Function-like set
g + (- (Omega --> (expect (g,v)))) is Relation-like Function-like set
dom (g - (Omega --> (expect (g,v)))) is Element of bool Omega
(dom g) /\ (dom (Omega --> (expect (g,v)))) is Element of bool Omega
abs (g - (Omega --> (expect (g,v)))) is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom (abs (g - (Omega --> (expect (g,v))))) is Element of bool Omega
(abs (g - (Omega --> (expect (g,v))))) to_power 2 is Relation-like Omega -defined REAL -valued Function-like V146() V147() V148() Element of bool [:Omega,REAL:]
dom ((abs (g - (Omega --> (expect (g,v))))) to_power 2) is Element of bool Omega
y is set
h . y is ext-real V38() V39() Element of REAL
(abs (g - (Omega --> (expect (g,v))))) . y is ext-real V38() V39() Element of REAL
((abs (g - (Omega --> (expect (g,v))))) . y) to_power 2 is ext-real V38() V39() Element of REAL
(g - (Omega --> (expect (g,v)))) . y is ext-real V38() V39() Element of REAL
abs ((g - (Omega --> (expect (g,v)))) . y) is ext-real V38() V39() Element of REAL
(abs ((g - (Omega --> (expect (g,v)))) . y)) to_power 2 is ext-real V38() V39() Element of REAL
g . y is ext-real V38() V39() Element of REAL
(Omega --> (expect (g,v))) . y is ext-real V38() V39() Element of REAL
(g . y) - ((Omega --> (expect (g,v))) . y) is ext-real V38() V39() Element of REAL
abs ((g . y) - ((Omega --> (expect (g,v))) . y)) is ext-real V38() V39() Element of REAL
(abs ((g . y) - ((Omega --> (expect (g,v))) . y))) to_power 2 is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
g . y is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is set
h . y is ext-real V38() V39() Element of REAL
(abs (g - (Omega --> (expect (g,v))))) . y is ext-real V38() V39() Element of REAL
((abs (g - (Omega --> (expect (g,v))))) . y) to_power 2 is ext-real V38() V39() Element of REAL
(g - (Omega --> (expect (g,v)))) . y is ext-real V38() V39() Element of REAL
abs ((g - (Omega --> (expect (g,v)))) . y) is ext-real V38() V39() Element of REAL
(abs ((g - (Omega --> (expect (g,v)))) . y)) to_power 2 is ext-real V38() V39() Element of REAL
g . y is ext-real V38() V39() Element of REAL
(Omega --> (expect (g,v))) . y is ext-real V38() V39() Element of REAL
(g . y) - ((Omega --> (expect (g,v))) . y) is ext-real V38() V39() Element of REAL
abs ((g . y) - ((Omega --> (expect (g,v))) . y)) is ext-real V38() V39() Element of REAL
(abs ((g . y) - ((Omega --> (expect (g,v))) . y))) to_power 2 is ext-real V38() V39() Element of REAL
(g . y) - (expect (g,v)) is ext-real V38() V39() Element of REAL
abs ((g . y) - (expect (g,v))) is ext-real V38() V39() Element of REAL
(abs ((g . y) - (expect (g,v)))) to_power 2 is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
y is Element of Omega
h . y is ext-real V38() V39() Element of REAL
Omega is non empty finite set
[:Omega,REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:Omega,REAL:] is non empty non trivial non finite set
bool Omega is non empty finite V31() set
[:(bool Omega),REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:(bool Omega),REAL:] is non empty non trivial non finite set
Trivial-SigmaField Omega is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
bool (bool Omega) is non empty finite V31() set
Sigma is Relation-like Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:Omega,REAL:]
v is Relation-like bool Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:(bool Omega),REAL:]
v . Omega is ext-real V38() V39() Element of REAL
v1 is finite Event of Trivial-SigmaField Omega
g is finite Event of Trivial-SigmaField Omega
v1 \/ g is finite Event of Trivial-SigmaField Omega
v . (v1 \/ g) is ext-real V38() V39() Element of REAL
v . v1 is ext-real V38() V39() Element of REAL
v . g is ext-real V38() V39() Element of REAL
(v . v1) + (v . g) is ext-real V38() V39() Element of REAL
dom Sigma is non empty finite Element of bool Omega
u is finite Element of bool Omega
u1 is finite Element of bool Omega
u \/ u1 is finite Element of bool Omega
setopfunc ((u \/ u1),Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
setopfunc (u,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
setopfunc (u1,Omega,REAL,Sigma,addreal) is ext-real V38() V39() Element of REAL
addreal . ((setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))) is ext-real V38() V39() Element of REAL
[(setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))] is set
{(setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))} is non empty finite V139() V140() V141() set
{(setopfunc (u,Omega,REAL,Sigma,addreal))} is non empty trivial finite 1 -element V139() V140() V141() set
{{(setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))},{(setopfunc (u,Omega,REAL,Sigma,addreal))}} is non empty finite V31() set
addreal . [(setopfunc (u,Omega,REAL,Sigma,addreal)),(setopfunc (u1,Omega,REAL,Sigma,addreal))] is ext-real V38() V39() set
addreal . ((setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)) is ext-real V38() V39() Element of REAL
[(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)] is set
{(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)} is non empty finite V139() V140() V141() set
{{(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)},{(setopfunc (u,Omega,REAL,Sigma,addreal))}} is non empty finite V31() set
addreal . [(setopfunc (u,Omega,REAL,Sigma,addreal)),(v . g)] is ext-real V38() V39() set
addreal . ((v . v1),(v . g)) is ext-real V38() V39() Element of REAL
[(v . v1),(v . g)] is set
{(v . v1),(v . g)} is non empty finite V139() V140() V141() set
{(v . v1)} is non empty trivial finite 1 -element V139() V140() V141() set
{{(v . v1),(v . g)},{(v . v1)}} is non empty finite V31() set
addreal . [(v . v1),(v . g)] is ext-real V38() V39() set
v1 is finite Event of Trivial-SigmaField Omega
v . v1 is ext-real V38() V39() Element of REAL
K264(Omega) is non empty finite V31() Element of bool (bool Omega)
[:NAT,K264(Omega):] is Relation-like non empty non trivial non finite set
bool [:NAT,K264(Omega):] is non empty non trivial non finite set
v1 is Relation-like NAT -defined Trivial-SigmaField Omega -valued K264(Omega) -valued Function-like non empty total quasi_total Element of bool [:NAT,K264(Omega):]
v * v1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() Element of bool [:NAT,REAL:]
lim (v * v1) is ext-real V38() V39() Element of REAL
Intersection v1 is finite Element of bool Omega
v . (Intersection v1) is ext-real V38() V39() Element of REAL
g is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
u is V17() V18() V19() V23() ext-real non negative finite cardinal V38() V39() V104() V139() V140() V141() V142() V143() V144() V161() Element of NAT
dom v1 is non empty V139() V140() V141() V142() V143() V144() Element of bool NAT
(v * v1) . u is ext-real V38() V39() Element of REAL
v1 . u is finite Element of Trivial-SigmaField Omega
v . (v1 . u) is ext-real V38() V39() Element of REAL
Omega is non empty finite set
Trivial-SigmaField Omega is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
bool Omega is non empty finite V31() set
bool (bool Omega) is non empty finite V31() set
Sigma is non empty finite set
Trivial-SigmaField Sigma is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Sigma) Element of bool (bool Sigma)
bool Sigma is non empty finite V31() set
bool (bool Sigma) is non empty finite V31() set
[:Omega,Sigma:] is Relation-like non empty finite set
[:[:Omega,Sigma:],REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:[:Omega,Sigma:],REAL:] is non empty non trivial non finite set
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
g is Relation-like Function-like set
dom g is set
u is set
g . u is set
u1 is set
h is set
[u1,h] is set
{u1,h} is non empty finite set
{u1} is non empty trivial finite 1 -element set
{{u1,h},{u1}} is non empty finite V31() set
g . (u1,h) is set
g . [u1,h] is set
v . {u1} is ext-real V38() V39() Element of REAL
{h} is non empty trivial finite 1 -element set
v1 . {h} is ext-real V38() V39() Element of REAL
(v . {u1}) * (v1 . {h}) is ext-real V38() V39() Element of REAL
u is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
u1 is set
h is set
u . (u1,h) is set
[u1,h] is set
{u1,h} is non empty finite set
{u1} is non empty trivial finite 1 -element set
{{u1,h},{u1}} is non empty finite V31() set
u . [u1,h] is ext-real V38() V39() set
v . {u1} is ext-real V38() V39() Element of REAL
{h} is non empty trivial finite 1 -element set
v1 . {h} is ext-real V38() V39() Element of REAL
(v . {u1}) * (v1 . {h}) is ext-real V38() V39() Element of REAL
Omega is non empty finite set
Trivial-SigmaField Omega is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Omega) Element of bool (bool Omega)
bool Omega is non empty finite V31() set
bool (bool Omega) is non empty finite V31() set
Sigma is non empty finite set
Trivial-SigmaField Sigma is non empty finite V31() compl-closed sigma-multiplicative V184() V185() V186() V203(Sigma) Element of bool (bool Sigma)
bool Sigma is non empty finite V31() set
bool (bool Sigma) is non empty finite V31() set
[:Omega,Sigma:] is Relation-like non empty finite set
[:[:Omega,Sigma:],REAL:] is Relation-like non empty non trivial non finite V146() V147() V148() set
bool [:[:Omega,Sigma:],REAL:] is non empty non trivial non finite set
v is Relation-like Trivial-SigmaField Omega -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Omega
v1 is Relation-like Trivial-SigmaField Sigma -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Probability of Trivial-SigmaField Sigma
g is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
u is Relation-like [:Omega,Sigma:] -defined REAL -valued Function-like non empty finite total quasi_total V146() V147() V148() Element of bool [:[:Omega,Sigma:],REAL:]
dom g is Relation-like Omega -defined Sigma -valued non empty finite Element of bool [:Omega,Sigma:]
bool [:Omega,Sigma:] is non empty finite V31() set
dom u is Relation-like Omega -defined Sigma -valued non empty finite Element of bool [:Omega,Sigma:]
u1 is set
h is set
y is set
[h,y] is set
{h,y} is non empty finite set
{h} is non empty trivial finite 1 -element set
{{h,y},{h}} is non empty finite V31()