rvsum_3.miz



    begin

    theorem :: RVSUM_3:1

    

     ProdMon: for x,y,z,w be Real st |.(x - y).| < |.(z - w).| holds ((x - y) ^2 ) < ((z - w) ^2 )

    proof

      let x,y,z,w be Real;

      

       A2: ( |.(x - y).| ^2 ) = ((x - y) ^2 ) by COMPLEX1: 75;

      assume |.(x - y).| < |.(z - w).|;

      then ( |.(x - y).| ^2 ) < ( |.(z - w).| ^2 ) by SQUARE_1: 16;

      hence thesis by COMPLEX1: 75, A2;

    end;

    theorem :: RVSUM_3:2

    for x,y,z,w be Real st |.(x - y).| < |.(z - w).| & (x + y) = (z + w) holds (x * y) > (z * w)

    proof

      let x,y,z,w be Real;

      assume

       A1: |.(x - y).| < |.(z - w).| & (x + y) = (z + w);

      ((x - y) ^2 ) < ((z - w) ^2 ) by A1, ProdMon;

      then (((x + y) ^2 ) - ((x - y) ^2 )) > (((z + w) ^2 ) - ((z - w) ^2 )) by A1, XREAL_1: 15;

      then (4 * (x * y)) > (4 * (z * w));

      hence thesis by XREAL_1: 64;

    end;

    notation

      let f be real-valued FinSequence;

      synonym f is positive for f is positive-yielding;

    end

    definition

      let f be real-valued FinSequence;

      :: original: positive

      redefine

      :: RVSUM_3:def1

      attr f is positive means

      : PosDef: for n be Nat st n in ( dom f) holds (f . n) > 0 ;

      compatibility

      proof

        thus f is positive implies for n be Nat st n in ( dom f) holds (f . n) > 0 by FUNCT_1: 3;

        assume

         A3: for n be Nat st n in ( dom f) holds (f . n) > 0 ;

        for r be Real st r in ( rng f) holds 0 < r

        proof

          let r be Real;

          assume r in ( rng f);

          then

          consider x be object such that

           A2: x in ( dom f) & r = (f . x) by FUNCT_1:def 3;

          reconsider n = x as Nat by A2;

          thus thesis by A2, A3;

        end;

        hence thesis;

      end;

    end

    registration

      cluster non empty constant positive for real-valued FinSequence;

      existence

      proof

        set f = <*1*>;

        for n be Nat st n in ( dom f) holds (f . n) > 0

        proof

          let n be Nat;

          assume n in ( dom f);

          then n in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

          then n = 1 by TARSKI:def 1;

          hence thesis by FINSEQ_1:def 8;

        end;

        then f is non empty positive;

        hence thesis;

      end;

      cluster non empty non constant positive for real-valued FinSequence;

      existence

      proof

        set f = <*1, 2*>;

        for n be Nat st n in ( dom f) holds (f . n) > 0

        proof

          let n be Nat;

          assume n in ( dom f);

          then n in ( Seg ( len f)) by FINSEQ_1:def 3;

          then n in {1, 2} by FINSEQ_1: 2, FINSEQ_1: 44;

          then n = 1 or n = 2 by TARSKI:def 2;

          hence thesis by FINSEQ_1: 44;

        end;

        then

         A1: f is non empty positive;

        ( dom f) = {1, 2} by FINSEQ_1: 92;

        then

         A2: 1 in ( dom f) & 2 in ( dom f) by TARSKI:def 2;

        (f . 1) = 1 & (f . 2) = 2 by FINSEQ_1: 44;

        then f is non constant by A2;

        hence thesis by A1;

      end;

    end

    registration

      let f be non empty real-valued FinSequence;

      let n be Nat;

      cluster (f | ( Seg n)) -> real-valued;

      coherence ;

    end

    registration

      let f be positive non empty real-valued FinSequence;

      let n be Nat;

      cluster (f | ( Seg n)) -> positive;

      coherence

      proof

        set g = (f | ( Seg n));

        for k be Nat st k in ( dom g) holds (g . k) > 0

        proof

          let k be Nat;

          

           A1: ( dom g) c= ( dom f) by RELAT_1: 60;

          assume

           A3: k in ( dom g);

          then (f . k) > 0 by PosDef, A1;

          hence thesis by FUNCT_1: 47, A3;

        end;

        hence thesis;

      end;

    end

    notation

      let f be FinSequence;

      synonym f is homogeneous for f is constant;

    end

    notation

      let f be FinSequence;

      antonym f is heterogeneous for f is homogeneous;

    end

    theorem :: RVSUM_3:3

    

     Th83: for R1,R2 be real-valued FinSequence st ( len R1) = ( len R2) & (for j be Nat st j in ( Seg ( len R1)) holds (R1 . j) <= (R2 . j)) & (ex j be Nat st j in ( Seg ( len R1)) & (R1 . j) < (R2 . j)) holds ( Sum R1) < ( Sum R2)

    proof

      let R1,R2 be real-valued FinSequence;

      set i = ( len R1);

      assume

       A1: ( len R1) = ( len R2) & (for j be Nat st j in ( Seg i) holds (R1 . j) <= (R2 . j)) & (ex j be Nat st j in ( Seg i) & (R1 . j) < (R2 . j));

      reconsider w = ( len R1) as natural Number;

      R1 is FinSequence of REAL & R2 is FinSequence of REAL by RVSUM_1: 145;

      then

      reconsider r1 = R1, r2 = R2 as Element of (w -tuples_on REAL ) by A1, FINSEQ_2: 92;

      ( Sum r1) < ( Sum r2) by A1, RVSUM_1: 83;

      hence thesis;

    end;

    theorem :: RVSUM_3:4

    for R1,R2 be real-valued FinSequence st (R1,R2) are_fiberwise_equipotent holds ( Product R1) = ( Product R2)

    proof

      let R1,R2 be real-valued FinSequence;

      defpred P[ Nat] means for f,g be FinSequence of REAL st (f,g) are_fiberwise_equipotent & ( len f) = $1 holds ( Product f) = ( Product g);

      assume

       A1: (R1,R2) are_fiberwise_equipotent ;

      

       A2: ( len R1) = ( len R1);

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: P[n];

        let f,g be FinSequence of REAL ;

        assume that

         A5: (f,g) are_fiberwise_equipotent and

         A6: ( len f) = (n + 1);

        set a = (f . (n + 1));

        

         A7: ( rng f) = ( rng g) by A5, CLASSES1: 75;

        ( 0 qua Nat + 1) <= (n + 1) by NAT_1: 13;

        then (n + 1) in ( dom f) by A6, FINSEQ_3: 25;

        then a in ( rng g) by A7, FUNCT_1:def 3;

        then

        consider m be Nat such that

         A8: m in ( dom g) and

         A9: (g . m) = a by FINSEQ_2: 10;

        set gg = (g /^ m), gm = (g | m);

        

         A11: 1 <= m by A8, FINSEQ_3: 25;

        ( max ( 0 ,(m - 1))) = (m - 1) by FINSEQ_2: 4, A8, FINSEQ_3: 25;

        then

        reconsider m1 = (m - 1) as Element of NAT by FINSEQ_2: 5;

        m = (m1 + 1);

        then

         A13: ( Seg m1) c= ( Seg m) by FINSEQ_1: 5, NAT_1: 11;

        m in ( Seg m) by A11;

        then

         WW: a = (gm . (m1 + 1)) by A8, A9, RFINSEQ: 6;

        m <= ( len g) by A8, FINSEQ_3: 25;

        then ( len gm) = m by FINSEQ_1: 59;

        then

         A14: gm = ((gm | m1) ^ <*a*>) by WW, RFINSEQ: 7;

        set fn = (f | n);

        

         A15: g = ((g | m) ^ (g /^ m)) by RFINSEQ: 8;

        

         A16: (gm | m1) = (g | (( Seg m) /\ ( Seg m1))) by RELAT_1: 71

        .= (g | m1) by A13, XBOOLE_1: 28;

        

         A17: f = (fn ^ <*a*>) by A6, RFINSEQ: 7;

        now

          let x be object;

          ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A5;

          

          then (( card (fn " {x})) + ( card ( <*a*> " {x}))) = ( card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})) by A15, A14, A16, A17, FINSEQ_3: 57

          .= (( card (((g | m1) ^ <*a*>) " {x})) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ( <*a*> " {x}))) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ((g /^ m) " {x}))) + ( card ( <*a*> " {x})))

          .= (( card (((g | m1) ^ (g /^ m)) " {x})) + ( card ( <*a*> " {x}))) by FINSEQ_3: 57;

          hence ( card ( Coim (fn,x))) = ( card ( Coim (((g | m1) ^ (g /^ m)),x)));

        end;

        then

         A18: (fn,((g | m1) ^ (g /^ m))) are_fiberwise_equipotent ;

        ( len fn) = n by A6, FINSEQ_1: 59, NAT_1: 11;

        then ( Product fn) = ( Product ((g | m1) ^ gg)) by A4, A18;

        

        hence ( Product f) = (( Product ((g | m1) ^ gg)) * ( Product <*a*>)) by A17, RVSUM_1: 97

        .= ((( Product (g | m1)) * ( Product gg)) * ( Product <*a*>)) by RVSUM_1: 97

        .= ((( Product (g | m1)) * ( Product <*a*>)) * ( Product gg))

        .= (( Product gm) * ( Product gg)) by A14, A16, RVSUM_1: 97

        .= ( Product g) by A15, RVSUM_1: 97;

      end;

      

       A19: P[ 0 ]

      proof

        let f,g be FinSequence of REAL ;

        assume

         a: (f,g) are_fiberwise_equipotent & ( len f) = 0 ;

        then

         A20: ( len g) = 0 & f = ( <*> REAL ) by RFINSEQ: 3;

        g = ( <*> REAL ) by RFINSEQ: 3, a;

        hence thesis by A20;

      end;

      

       A4: for n be Nat holds P[n] from NAT_1:sch 2( A19, A3);

      R1 is FinSequence of REAL & R2 is FinSequence of REAL by RVSUM_1: 145;

      hence thesis by A1, A2, A4;

    end;

    begin

    definition

      let f be real-valued FinSequence;

      :: RVSUM_3:def2

      func Mean f -> real number equals (( Sum f) / ( len f));

      coherence ;

    end

    definition

      let f be positive real-valued FinSequence;

      :: RVSUM_3:def3

      func GMean f -> real number equals (( len f) -root ( Product f));

      coherence by TARSKI: 1;

    end

    theorem :: RVSUM_3:5

    

     Huk1: for f be real-valued FinSequence holds ( Sum f) = (( len f) * ( Mean f))

    proof

      let f be real-valued FinSequence;

      per cases ;

        suppose ( len f) <> 0 ;

        hence thesis by XCMPLX_1: 87;

      end;

        suppose ( len f) = 0 ;

        then f = ( <*> REAL );

        hence thesis by RVSUM_1: 72;

      end;

    end;

    theorem :: RVSUM_3:6

    for f be real-valued FinSequence holds ( Mean (f ^ <*( Mean f)*>)) = ( Mean f)

    proof

      let f be real-valued FinSequence;

      ( Mean (f ^ <*( Mean f)*>)) = ((( Sum f) + ( Mean f)) / ( len (f ^ <*( Mean f)*>))) by RVSUM_1: 74

      .= ((( Sum f) + ( Mean f)) / (( len f) + ( len <*( Mean f)*>))) by FINSEQ_1: 22

      .= ((( Sum f) + ( Mean f)) / (( len f) + 1)) by FINSEQ_1: 39

      .= (((( len f) * ( Mean f)) + ( Mean f)) / (( len f) + 1)) by Huk1

      .= ((( Mean f) * (( len f) + 1)) / (( len f) + 1))

      .= ( Mean f) by XCMPLX_1: 89;

      hence thesis;

    end;

    registration

      let f be non empty constant real-valued FinSequence;

      cluster ( the_value_of f) -> real;

      coherence

      proof

        consider x be set such that

         A1: x in ( dom f) & ( the_value_of f) = (f . x) by FUNCT_1:def 12;

        thus thesis by A1;

      end;

    end

    theorem :: RVSUM_3:7

    

     ConstantSum: for f be non empty constant real-valued FinSequence holds ( Sum f) = (( the_value_of f) * ( len f))

    proof

      let f be non empty constant real-valued FinSequence;

      set r = ( the_value_of f), i = ( len f);

      f = (( dom f) --> r) by FUNCOP_1: 80

      .= (i |-> r) by FINSEQ_1:def 3;

      hence thesis by RVSUM_1: 80;

    end;

    theorem :: RVSUM_3:8

    

     ConstantProduct: for f be non empty constant real-valued FinSequence holds ( Product f) = (( the_value_of f) |^ ( len f))

    proof

      let f be non empty constant real-valued FinSequence;

      set r = ( the_value_of f), i = ( len f);

      f = (( dom f) --> r) by FUNCOP_1: 80

      .= (i |-> r) by FINSEQ_1:def 3;

      hence thesis by NEWTON:def 1;

    end;

    theorem :: RVSUM_3:9

    

     ConstantMean: for f be non empty constant real-valued FinSequence holds ( Mean f) = ( the_value_of f)

    proof

      let f be non empty constant real-valued FinSequence;

      reconsider v = ( the_value_of f) as Real;

      ( Mean f) = ((( len f) * v) / ( len f)) by ConstantSum

      .= (v * (( len f) / ( len f))) by XCMPLX_1: 74

      .= (v * 1) by XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: RVSUM_3:10

    

     PosLeq: for f be non empty constant positive real-valued FinSequence holds ( the_value_of f) > 0

    proof

      let f be non empty constant positive real-valued FinSequence;

      consider x be set such that

       A1: x in ( dom f) & ( the_value_of f) = (f . x) by FUNCT_1:def 12;

      thus thesis by A1, PosDef;

    end;

    theorem :: RVSUM_3:11

    

     ConstantGMean: for f be non empty constant positive real-valued FinSequence holds ( GMean f) = ( the_value_of f)

    proof

      let f be non empty constant positive real-valued FinSequence;

      reconsider v = ( the_value_of f) as Real;

      

       A3: ( len f) >= 1 by NAT_1: 14;

      

       A4: v >= 0 by PosLeq;

      ( Product f) = (v |^ ( len f)) by ConstantProduct;

      hence thesis by A4, A3, POWER: 4;

    end;

    registration

      let f be non empty positive real-valued FinSequence;

      cluster ( Mean f) -> positive;

      coherence

      proof

        

         B1: for i be Nat st i in ( dom f) holds 0 <= (f . i) by PosDef;

        ex i be Nat st i in ( dom f) & 0 < (f . i)

        proof

          take i = 1;

          1 in ( dom f) by FINSEQ_5: 6;

          hence thesis by PosDef;

        end;

        then ( Sum f) > 0 by B1, RVSUM_1: 85;

        hence thesis;

      end;

    end

    registration

      let f be non empty positive real-valued FinSequence;

      cluster ( Product f) -> positive;

      coherence

      proof

        reconsider F = f as FinSequence of REAL by RVSUM_1: 145;

        for k be Element of NAT st k in ( dom F) holds (F . k) > 0 by PosDef;

        hence thesis by NAT_4: 42;

      end;

    end

    registration

      let f be positive non empty real-valued FinSequence;

      cluster ( GMean f) -> positive;

      coherence

      proof

        

         A2: ( len f) >= 1 by NAT_1: 14;

        (( len f) -root ( Product f)) = (( len f) -Root ( Product f)) by POWER:def 1, NAT_1: 14;

        hence thesis by A2, PREPOWER:def 2;

      end;

    end

    begin

    definition

      let f be real-valued FinSequence;

      :: RVSUM_3:def4

      func HetSet f -> Subset of NAT equals { n where n be Nat : n in ( dom f) & (f . n) <> ( Mean f) };

      coherence

      proof

        

         A3: { n where n be Nat : n in ( dom f) & (f . n) <> ( Mean f) } c= ( dom f)

        proof

          let x be object;

          assume x in { n where n be Nat : n in ( dom f) & (f . n) <> ( Mean f) };

          then

          consider n be Nat such that

           A2: x = n & n in ( dom f) & (f . n) <> ( Mean f);

          thus thesis by A2;

        end;

        ( dom f) c= NAT ;

        then { n where n be Nat : n in ( dom f) & (f . n) <> ( Mean f) } c= NAT by A3;

        hence thesis;

      end;

    end

    registration

      let f be real-valued FinSequence;

      cluster ( HetSet f) -> finite;

      coherence

      proof

        { n where n be Nat : n in ( dom f) & (f . n) <> ( Mean f) } c= ( dom f)

        proof

          let x be object;

          assume x in { n where n be Nat : n in ( dom f) & (f . n) <> ( Mean f) };

          then ex n be Nat st x = n & n in ( dom f) & (f . n) <> ( Mean f);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let f be positive non empty real-valued FinSequence;

      cluster ( HetSet f) -> bounded_above bounded_below real-membered;

      coherence ;

    end

    definition

      let f be real-valued FinSequence;

      :: RVSUM_3:def5

      func Het f -> Nat equals ( card ( HetSet f));

      coherence ;

    end

    theorem :: RVSUM_3:12

    

     HetHomo: for f be real-valued FinSequence st ( Het f) = 0 holds f is homogeneous

    proof

      let f be real-valued FinSequence;

      assume

       A1: ( Het f) = 0 ;

      set X = { n where n be Nat : n in ( dom f) & (f . n) <> ( Mean f) };

      assume

       a4: f is heterogeneous;

      

       A5: for n be Nat st n in ( dom f) holds (f . n) = ( Mean f)

      proof

        let n be Nat;

        assume

         A2: n in ( dom f);

        (f . n) = ( Mean f)

        proof

          assume (f . n) <> ( Mean f);

          then n in X by A2;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      for x,y be object st x in ( dom f) & y in ( dom f) holds (f . x) = (f . y)

      proof

        let x,y be object;

        assume

         B1: x in ( dom f) & y in ( dom f);

        then

        reconsider xx = x, yy = y as Nat;

        (f . xx) = ( Mean f) by A5, B1;

        hence thesis by A5, B1;

      end;

      hence thesis by a4;

    end;

    theorem :: RVSUM_3:13

    

     HetHetero: for f be non empty real-valued FinSequence st ( Het f) <> 0 holds f is heterogeneous

    proof

      let f be non empty real-valued FinSequence;

      assume

       A1: ( Het f) <> 0 ;

      assume

       A3: f is homogeneous;

      then ( the_value_of f) = ( Mean f) by ConstantMean;

      then

      consider x be set such that

       A2: x in ( dom f) & ( Mean f) = (f . x) by FUNCT_1:def 12, A3;

      ( HetSet f) <> {} by A1;

      then

      consider y be object such that

       A5: y in ( HetSet f) by XBOOLE_0:def 1;

      consider z be Nat such that

       A6: z = y & z in ( dom f) & (f . z) <> ( Mean f) by A5;

      thus thesis by A3, A2, A6;

    end;

    registration

      let f be heterogeneous positive non empty real-valued FinSequence;

      cluster ( HetSet f) -> non empty;

      coherence

      proof

        ( Het f) <> 0 by HetHomo;

        hence thesis;

      end;

    end

    theorem :: RVSUM_3:14

    

     HetBase: for f be non empty homogeneous positive real-valued FinSequence holds ( Mean f) = ( GMean f)

    proof

      let f be non empty homogeneous positive real-valued FinSequence;

      ( the_value_of f) = ( Mean f) by ConstantMean;

      hence thesis by ConstantGMean;

    end;

    definition

      let f1,f2 be real-valued FinSequence;

      :: RVSUM_3:def6

      pred f1,f2 are_gamma-equivalent means ( len f1) = ( len f2) & ( Mean f1) = ( Mean f2);

      reflexivity ;

      symmetry ;

    end

    theorem :: RVSUM_3:15

    for f1,f2 be real-valued FinSequence st ( dom f1) = ( dom f2) & ( Sum f1) = ( Sum f2) holds (f1,f2) are_gamma-equivalent by FINSEQ_3: 29;

    definition

      let f be real-valued FinSequence;

      :: RVSUM_3:def7

      func MeanLess f -> Subset of NAT equals { n where n be Nat : n in ( dom f) & (f . n) < ( Mean f) };

      coherence

      proof

        

         A3: { n where n be Nat : n in ( dom f) & (f . n) < ( Mean f) } c= ( dom f)

        proof

          let x be object;

          assume x in { n where n be Nat : n in ( dom f) & (f . n) < ( Mean f) };

          then

          consider n be Nat such that

           A2: x = n & n in ( dom f) & (f . n) < ( Mean f);

          thus thesis by A2;

        end;

        ( dom f) c= NAT ;

        then { n where n be Nat : n in ( dom f) & (f . n) < ( Mean f) } c= NAT by A3;

        hence thesis;

      end;

      :: RVSUM_3:def8

      func MeanMore f -> Subset of NAT equals { n where n be Nat : n in ( dom f) & (f . n) > ( Mean f) };

      coherence

      proof

        

         A3: { n where n be Nat : n in ( dom f) & (f . n) > ( Mean f) } c= ( dom f)

        proof

          let x be object;

          assume x in { n where n be Nat : n in ( dom f) & (f . n) > ( Mean f) };

          then ex n be Nat st x = n & n in ( dom f) & (f . n) > ( Mean f);

          hence thesis;

        end;

        ( dom f) c= NAT ;

        then { n where n be Nat : n in ( dom f) & (f . n) > ( Mean f) } c= NAT by A3;

        hence thesis;

      end;

    end

    theorem :: RVSUM_3:16

    for f be real-valued FinSequence holds ( HetSet f) c= ( dom f)

    proof

      let f be real-valued FinSequence;

      let x be object;

      assume x in ( HetSet f);

      then ex n be Nat st x = n & n in ( dom f) & (f . n) <> ( Mean f);

      hence thesis;

    end;

    theorem :: RVSUM_3:17

    

     LessDom: for f be real-valued FinSequence holds ( MeanLess f) c= ( dom f)

    proof

      let f be real-valued FinSequence;

      let x be object;

      assume x in ( MeanLess f);

      then ex n be Nat st x = n & n in ( dom f) & (f . n) < ( Mean f);

      hence thesis;

    end;

    theorem :: RVSUM_3:18

    

     MoreDom: for f be real-valued FinSequence holds ( MeanMore f) c= ( dom f)

    proof

      let f be real-valued FinSequence;

      let x be object;

      assume x in ( MeanMore f);

      then ex n be Nat st x = n & n in ( dom f) & (f . n) > ( Mean f);

      hence thesis;

    end;

    theorem :: RVSUM_3:19

    

     MeanSum: for f be real-valued FinSequence holds ( HetSet f) = (( MeanLess f) \/ ( MeanMore f))

    proof

      let f be real-valued FinSequence;

      thus ( HetSet f) c= (( MeanLess f) \/ ( MeanMore f))

      proof

        let x be object;

        assume x in ( HetSet f);

        then

        consider i be Nat such that

         A1: i = x & i in ( dom f) & (f . i) <> ( Mean f);

        (f . i) < ( Mean f) or (f . i) > ( Mean f) by A1, XXREAL_0: 1;

        then i in ( MeanLess f) or i in ( MeanMore f) by A1;

        hence thesis by A1, XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in (( MeanLess f) \/ ( MeanMore f));

      per cases by XBOOLE_0:def 3;

        suppose x in ( MeanLess f);

        then ex i be Nat st i = x & i in ( dom f) & (f . i) < ( Mean f);

        hence thesis;

      end;

        suppose x in ( MeanMore f);

        then ex i be Nat st i = x & i in ( dom f) & (f . i) > ( Mean f);

        hence thesis;

      end;

    end;

    

     MeanL: for f be heterogeneous real-valued FinSequence holds ( MeanLess f) <> {}

    proof

      let f be heterogeneous real-valued FinSequence;

      ( Het f) <> {} by HetHomo;

      then ( HetSet f) <> {} ;

      then

      consider x be object such that

       A1: x in ( HetSet f) by XBOOLE_0: 7;

      x in (( MeanLess f) \/ ( MeanMore f)) by A1, MeanSum;

      per cases by XBOOLE_0:def 3;

        suppose x in ( MeanLess f);

        hence thesis;

      end;

        suppose x in ( MeanMore f);

        then

        consider n be Nat such that

         A2: x = n & n in ( dom f) & (f . n) > ( Mean f);

        reconsider R1 = (( len f) |-> ( Mean f)) as real-valued FinSequence;

        set ff = f;

        reconsider w = ( len R1) as Nat;

        ex i be Nat st i in ( dom f) & (ff . i) < ( Mean f)

        proof

          assume

           TT: for i be Nat st i in ( dom f) holds (ff . i) >= ( Mean f);

          

           G1: for j be Nat st j in ( Seg w) holds (R1 . j) <= (ff . j)

          proof

            let j be Nat;

            assume

             g0: j in ( Seg w);

            then

             G2: j in ( Seg ( len f)) by CARD_1:def 7;

            

             G3: j in ( dom f) by FINSEQ_1:def 3, CARD_1:def 7, g0;

            (R1 . j) = ( Mean f) by G2, FINSEQ_2: 57;

            hence thesis by TT, G3;

          end;

          ex j be Nat st j in ( Seg w) & (R1 . j) < (ff . j)

          proof

            take n;

            n in ( Seg ( len f)) by A2, FINSEQ_1:def 3;

            hence thesis by CARD_1:def 7, A2, FINSEQ_2: 57;

          end;

          then ( Sum R1) < ( Sum ff) by Th83, G1, CARD_1:def 7;

          then ( Sum ff) > (( len f) * ( Mean f)) by RVSUM_1: 80;

          hence thesis by Huk1;

        end;

        then

        consider m be Nat such that

         B1: m in ( dom f) & (f . m) < ( Mean f);

        m in ( MeanLess f) by B1;

        hence thesis;

      end;

    end;

    

     MeanM: for f be heterogeneous real-valued FinSequence holds ( MeanMore f) <> {}

    proof

      let f be heterogeneous real-valued FinSequence;

      ( Het f) <> {} by HetHomo;

      then ( HetSet f) <> {} ;

      then

      consider x be object such that

       A1: x in ( HetSet f) by XBOOLE_0: 7;

      x in (( MeanLess f) \/ ( MeanMore f)) by A1, MeanSum;

      per cases by XBOOLE_0:def 3;

        suppose x in ( MeanMore f);

        hence thesis;

      end;

        suppose x in ( MeanLess f);

        then

        consider n be Nat such that

         A2: x = n & n in ( dom f) & (f . n) < ( Mean f);

        reconsider R1 = (( len f) |-> ( Mean f)) as real-valued FinSequence;

        set ff = f;

        reconsider w = ( len R1) as Nat;

        ex i be Nat st i in ( dom f) & (ff . i) > ( Mean f)

        proof

          assume

           TT: for i be Nat st i in ( dom f) holds (ff . i) <= ( Mean f);

          

           G0: ( len R1) = ( len f) by CARD_1:def 7;

          

           G1: for j be Nat st j in ( Seg w) holds (R1 . j) >= (ff . j)

          proof

            let j be Nat;

            assume

             g0: j in ( Seg w);

            then

             G2: j in ( Seg ( len f)) by CARD_1:def 7;

            

             G3: j in ( dom f) by FINSEQ_1:def 3, g0, CARD_1:def 7;

            (R1 . j) = ( Mean f) by G2, FINSEQ_2: 57;

            hence thesis by TT, G3;

          end;

          ex j be Nat st j in ( Seg w) & (R1 . j) > (ff . j)

          proof

            take n;

            n in ( Seg ( len f)) by A2, FINSEQ_1:def 3;

            hence thesis by A2, FINSEQ_2: 57, CARD_1:def 7;

          end;

          then ( Sum R1) > ( Sum ff) by Th83, G1, G0;

          then ( Sum ff) < (( len f) * ( Mean f)) by RVSUM_1: 80;

          hence thesis by Huk1;

        end;

        then

        consider m be Nat such that

         B1: m in ( dom f) & (f . m) > ( Mean f);

        m in ( MeanMore f) by B1;

        hence thesis;

      end;

    end;

    registration

      let f be heterogeneous real-valued FinSequence;

      cluster ( MeanLess f) -> non empty;

      coherence by MeanL;

      cluster ( MeanMore f) -> non empty;

      coherence by MeanM;

    end

    registration

      let f be homogeneous real-valued FinSequence;

      cluster ( MeanLess f) -> empty;

      coherence

      proof

        per cases ;

          suppose f is empty;

          then ( dom f) = {} ;

          then ( MeanLess f) c= {} by LessDom;

          hence thesis;

        end;

          suppose

           AA: f is non empty;

          

           A0: ( HetSet f) = (( MeanLess f) \/ ( MeanMore f)) by MeanSum;

          ( MeanLess f) = {}

          proof

            assume ( MeanLess f) <> {} ;

            then

            consider x be object such that

             A1: x in ( MeanLess f) by XBOOLE_0: 7;

            ( Het f) <> 0 by A0, A1;

            hence thesis by HetHetero, AA;

          end;

          hence thesis;

        end;

      end;

      cluster ( MeanMore f) -> empty;

      coherence

      proof

        per cases ;

          suppose f is empty;

          then ( dom f) = {} ;

          then ( MeanMore f) c= {} by MoreDom;

          hence thesis;

        end;

          suppose

           AA: f is non empty;

          

           A0: ( HetSet f) = (( MeanLess f) \/ ( MeanMore f)) by MeanSum;

          ( MeanMore f) = {}

          proof

            assume ( MeanMore f) <> {} ;

            then

            consider x be object such that

             A1: x in ( MeanMore f) by XBOOLE_0: 7;

            ( Het f) <> 0 by A0, A1;

            hence thesis by HetHetero, AA;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: RVSUM_3:20

    

     MeanMiss: for f be heterogeneous non empty real-valued FinSequence holds ( MeanLess f) misses ( MeanMore f)

    proof

      let f be heterogeneous non empty real-valued FinSequence;

      assume ( MeanLess f) meets ( MeanMore f);

      then

      consider x be object such that

       A1: x in ( MeanLess f) & x in ( MeanMore f) by XBOOLE_0: 3;

      consider i be Nat such that

       A2: i = x & i in ( dom f) & (f . i) < ( Mean f) by A1;

      consider j be Nat such that

       A3: j = x & j in ( dom f) & (f . j) > ( Mean f) by A1;

      thus thesis by A2, A3;

    end;

    theorem :: RVSUM_3:21

    for f be heterogeneous non empty real-valued FinSequence holds ( Het f) >= 2

    proof

      let f be heterogeneous non empty real-valued FinSequence;

      set x = the Element of ( MeanLess f);

      set y = the Element of ( MeanMore f);

      ( HetSet f) = (( MeanLess f) \/ ( MeanMore f)) by MeanSum;

      then

       A0: x in ( HetSet f) & y in ( HetSet f) by XBOOLE_0:def 3;

      

       A4: x <> y by XBOOLE_0: 3, MeanMiss;

      

       A5: ( card {x, y}) = 2 by CARD_2: 57, A4;

      ( card ( Segm 2)) c= ( card ( Segm ( Het f))) by A5, ZFMISC_1: 32, A0, CARD_1: 11;

      hence thesis by NAT_1: 40;

    end;

    begin

    definition

      let f be Function, i,j be Nat, a,b be object;

      :: RVSUM_3:def9

      func Replace (f,i,j,a,b) -> Function equals ((f +* (i,a)) +* (j,b));

      coherence ;

    end

    theorem :: RVSUM_3:22

    

     DinoDom: for f be FinSequence, i,j be Nat, a,b be object holds ( dom ( Replace (f,i,j,a,b))) = ( dom f)

    proof

      let f be FinSequence, i,j be Nat, a,b be object;

      ( dom (f +* (i,a))) = ( dom f) by FUNCT_7: 30;

      hence thesis by FUNCT_7: 30;

    end;

    registration

      let f be real-valued FinSequence, i,j be Nat, a,b be Real;

      cluster ( Replace (f,i,j,a,b)) -> real-valued FinSequence-like;

      coherence ;

    end

    theorem :: RVSUM_3:23

    

     CopyForValued: for w be real-valued FinSequence, r be Real, i be Nat st i in ( dom w) holds (w +* (i,r)) = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i))

    proof

      let w be real-valued FinSequence, r be Real, i be Nat;

      reconsider ww = w as FinSequence of REAL by RVSUM_1: 145;

      reconsider rr = r as Element of REAL by XREAL_0:def 1;

      assume i in ( dom w);

      then (ww +* (i,rr)) = (((ww | (i -' 1)) ^ <*rr*>) ^ (ww /^ i)) by FUNCT_7: 98;

      hence thesis;

    end;

    theorem :: RVSUM_3:24

    

     SumA: for f be real-valued FinSequence, i be Nat, a be Real st i in ( dom f) holds ( Sum (f +* (i,a))) = ((( Sum f) - (f . i)) + a)

    proof

      let f be real-valued FinSequence, i be Nat, a be Real;

      reconsider w = f as FinSequence of REAL by RVSUM_1: 145;

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      assume

       A1: i in ( dom f);

      

      then

       Z1: ( Sum (w +* (i,a))) = ( Sum (((w | (i -' 1)) ^ <*aa*>) ^ (w /^ i))) by CopyForValued

      .= (( Sum ((w | (i -' 1)) ^ <*aa*>)) + ( Sum (w /^ i))) by RVSUM_1: 75

      .= ((( Sum (w | (i -' 1))) + ( Sum <*aa*>)) + ( Sum (w /^ i))) by RVSUM_1: 75

      .= ((( Sum (w | (i -' 1))) + aa) + ( Sum (w /^ i))) by RVSUM_1: 73

      .= (aa + (( Sum (w | (i -' 1))) + ( Sum (w /^ i))))

      .= (aa + ( Sum ((w | (i -' 1)) ^ (w /^ i)))) by RVSUM_1: 75;

      reconsider fi = (f . i) as Real;

      1 <= i & i <= ( len w) by A1, FINSEQ_3: 25;

      

      then ( Sum w) = ( Sum (((w | (i -' 1)) ^ <*(f . i)*>) ^ (w /^ i))) by FINSEQ_5: 84

      .= (( Sum ((w | (i -' 1)) ^ <*(f . i)*>)) + ( Sum (w /^ i))) by RVSUM_1: 75

      .= ((( Sum (w | (i -' 1))) + ( Sum <*(f . i)*>)) + ( Sum (w /^ i))) by RVSUM_1: 75

      .= ((( Sum (w | (i -' 1))) + fi) + ( Sum (w /^ i))) by RVSUM_1: 73

      .= (fi + (( Sum (w | (i -' 1))) + ( Sum (w /^ i))))

      .= (fi + ( Sum ((w | (i -' 1)) ^ (w /^ i)))) by RVSUM_1: 75;

      hence thesis by Z1;

    end;

    theorem :: RVSUM_3:25

    

     ProductA: for f be positive real-valued FinSequence, i be Nat, a be Real st i in ( dom f) holds ( Product (f +* (i,a))) = ((( Product f) * a) / (f . i))

    proof

      let f be positive real-valued FinSequence, i be Nat, a be Real;

      reconsider w = f as FinSequence of REAL by RVSUM_1: 145;

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      assume

       A1: i in ( dom f);

      

      then

       Z1: ( Product (w +* (i,a))) = ( Product (((w | (i -' 1)) ^ <*aa*>) ^ (w /^ i))) by CopyForValued

      .= (( Product ((w | (i -' 1)) ^ <*aa*>)) * ( Product (w /^ i))) by RVSUM_1: 97

      .= ((( Product (w | (i -' 1))) * ( Product <*aa*>)) * ( Product (w /^ i))) by RVSUM_1: 97

      .= (aa * (( Product (w | (i -' 1))) * ( Product (w /^ i))))

      .= (aa * ( Product ((w | (i -' 1)) ^ (w /^ i)))) by RVSUM_1: 97;

      reconsider fi = (f . i) as Real;

      

       ZZ: fi <> 0 by A1, PosDef;

      1 <= i & i <= ( len w) by A1, FINSEQ_3: 25;

      

      then

       zz: ( Product w) = ( Product (((w | (i -' 1)) ^ <*(f . i)*>) ^ (w /^ i))) by FINSEQ_5: 84

      .= (( Product ((w | (i -' 1)) ^ <*(f . i)*>)) * ( Product (w /^ i))) by RVSUM_1: 97

      .= ((( Product (w | (i -' 1))) * ( Product <*(f . i)*>)) * ( Product (w /^ i))) by RVSUM_1: 97

      .= (fi * (( Product (w | (i -' 1))) * ( Product (w /^ i))))

      .= (fi * ( Product ((w | (i -' 1)) ^ (w /^ i)))) by RVSUM_1: 97;

      ( Product (w +* (i,a))) = (aa * (( Product w) / fi)) by ZZ, XCMPLX_1: 89, zz, Z1

      .= (aa * (( Product w) * (1 / fi))) by XCMPLX_1: 99

      .= ((( Product w) * aa) * (1 / fi))

      .= ((( Product f) * a) / (f . i)) by XCMPLX_1: 99;

      hence thesis;

    end;

    theorem :: RVSUM_3:26

    

     SumReplace: for f be real-valued FinSequence, i,j be Nat, a,b be Real st i in ( dom f) & j in ( dom f) & i <> j holds ( Sum ( Replace (f,i,j,a,b))) = ((((( Sum f) - (f . i)) - (f . j)) + a) + b)

    proof

      let f be real-valued FinSequence, i,j be Nat, a,b be Real;

      assume

       A0: i in ( dom f) & j in ( dom f) & i <> j;

      

       A1: j in ( dom (f +* (i,a))) by A0, FUNCT_7: 30;

      ( Sum ( Replace (f,i,j,a,b))) = ((( Sum (f +* (i,a))) - ((f +* (i,a)) . j)) + b) by A1, SumA

      .= ((( Sum (f +* (i,a))) - (f . j)) + b) by FUNCT_7: 32, A0

      .= ((((( Sum f) - (f . i)) + a) - (f . j)) + b) by A0, SumA

      .= (((( Sum f) - (f . i)) + (a - (f . j))) + b);

      hence thesis;

    end;

    theorem :: RVSUM_3:27

    

     ProdReplace: for f be positive real-valued FinSequence, i,j be Nat, a,b be positive Real st i in ( dom f) & j in ( dom f) & i <> j holds ( Product ( Replace (f,i,j,a,b))) = (((( Product f) * a) * b) / ((f . i) * (f . j)))

    proof

      let f be positive real-valued FinSequence, i,j be Nat, a,b be positive Real;

      for n be Nat st n in ( dom (f +* (i,a))) holds ((f +* (i,a)) . n) > 0

      proof

        let n be Nat;

        assume n in ( dom (f +* (i,a)));

        then

         A2: n in ( dom f) by FUNCT_7: 30;

        per cases ;

          suppose n = i;

          hence thesis by A2, FUNCT_7: 31;

        end;

          suppose n <> i;

          then ((f +* (i,a)) . n) = (f . n) by FUNCT_7: 32;

          hence thesis by PosDef, A2;

        end;

      end;

      then

       S1: (f +* (i,a)) is positive;

      assume

       A0: i in ( dom f) & j in ( dom f) & i <> j;

      

       A1: j in ( dom (f +* (i,a))) by A0, FUNCT_7: 30;

      ( Product ( Replace (f,i,j,a,b))) = ((( Product (f +* (i,a))) * b) / ((f +* (i,a)) . j)) by A1, ProductA, S1

      .= ((( Product (f +* (i,a))) * b) / (f . j)) by FUNCT_7: 32, A0

      .= ((((( Product f) * a) / (f . i)) * b) / (f . j)) by A0, ProductA

      .= ((((( Product f) * a) * (1 / (f . i))) * b) / (f . j)) by XCMPLX_1: 99

      .= ((((( Product f) * a) * b) * (1 / (f . i))) * (1 / (f . j))) by XCMPLX_1: 99

      .= ((((( Product f) * a) * b) / (f . i)) * (1 / (f . j))) by XCMPLX_1: 99

      .= ((((( Product f) * a) * b) / (f . i)) / (f . j)) by XCMPLX_1: 99

      .= (((( Product f) * a) * b) / ((f . i) * (f . j))) by XCMPLX_1: 78;

      hence thesis;

    end;

    theorem :: RVSUM_3:28

    

     ReplaceGamma: for f be real-valued FinSequence, i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j holds (f,( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f))))) are_gamma-equivalent

    proof

      let f be real-valued FinSequence, i,j be Nat;

      set a = ( Mean f);

      set b = (((f . i) + (f . j)) - ( Mean f));

      assume

       A1: i in ( dom f) & j in ( dom f) & i <> j;

      

       A2: ( dom f) = ( dom ( Replace (f,i,j,a,b))) by DinoDom;

      ( Sum ( Replace (f,i,j,a,b))) = ((((( Sum f) - (f . i)) - (f . j)) + a) + b) by SumReplace, A1

      .= ( Sum f);

      hence thesis by FINSEQ_3: 29, A2;

    end;

    theorem :: RVSUM_3:29

    

     ReplaceValue: for f be real-valued FinSequence, i,j,k be Nat, a,b be Real st i in ( dom f) & j in ( dom f) & k in ( dom f) & i <> j & (k <> i & k <> j) holds (( Replace (f,i,j,a,b)) . k) = (f . k)

    proof

      let f be real-valued FinSequence, i,j,k be Nat, a,b be Real;

      assume

       A1: i in ( dom f) & j in ( dom f) & k in ( dom f) & i <> j & (k <> i & k <> j);

      (( Replace (f,i,j,a,b)) . k) = ((f +* (i,a)) . k) by A1, FUNCT_7: 32

      .= (f . k) by A1, FUNCT_7: 32;

      hence thesis;

    end;

    theorem :: RVSUM_3:30

    

     ReplaceValue2: for f be FinSequence, i,j be Nat, a,b be object st i in ( dom f) & j in ( dom f) & i <> j holds (( Replace (f,i,j,a,b)) . j) = b

    proof

      let f be FinSequence, i,j be Nat, a,b be object;

      set g = ( Replace (f,i,j,a,b));

      assume i in ( dom f) & j in ( dom f) & i <> j;

      then j in ( dom (f +* (i,a))) by FUNCT_7: 30;

      hence thesis by FUNCT_7: 31;

    end;

    theorem :: RVSUM_3:31

    

     ReplaceValue3: for f be FinSequence, i,j be Nat, a,b be object st i in ( dom f) & j in ( dom f) & i <> j holds (( Replace (f,i,j,a,b)) . i) = a

    proof

      let f be FinSequence, i,j be Nat, a,b be object;

      set g = ( Replace (f,i,j,a,b));

      assume

       A1: i in ( dom f) & j in ( dom f) & i <> j;

      

      then (g . i) = ((f +* (i,a)) . i) by FUNCT_7: 32

      .= a by A1, FUNCT_7: 31;

      hence thesis;

    end;

    theorem :: RVSUM_3:32

    

     HetMono: for f be real-valued FinSequence, i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j & (f . i) <> ( Mean f) & (f . j) <> ( Mean f) holds ( Het f) > ( Het ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))))

    proof

      let f be real-valued FinSequence, i,j be Nat;

      assume

       A0: i in ( dom f) & j in ( dom f) & i <> j;

      assume

       FF: (f . i) <> ( Mean f) & (f . j) <> ( Mean f);

      set g = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f))));

      

       zz: (f,g) are_gamma-equivalent by ReplaceGamma, A0;

      set a = ( Mean f);

      set b = (((f . i) + (f . j)) - ( Mean f));

      

       FX: ( HetSet g) <> ( HetSet f)

      proof

        assume

         h2: ( HetSet g) = ( HetSet f);

         not i in { n1 where n1 be Nat : n1 in ( dom g) & (g . n1) <> ( Mean g) }

        proof

          assume i in { n1 where n1 be Nat : n1 in ( dom g) & (g . n1) <> ( Mean g) };

          then

          consider n2 be Nat such that

           G1: n2 = i & n2 in ( dom g) & (g . n2) <> ( Mean g);

          thus thesis by zz, ReplaceValue3, A0, G1;

        end;

        hence thesis by h2, FF, A0;

      end;

      ( HetSet g) c= ( HetSet f)

      proof

        let x be object;

        assume x in ( HetSet g);

        then

        consider n1 be Nat such that

         A1: n1 = x & n1 in ( dom g) & (g . n1) <> ( Mean g);

        

         A2: n1 in ( dom f) by A1, DinoDom;

        (f . n1) <> ( Mean f)

        proof

          per cases ;

            suppose n1 = i;

            hence thesis by A1, zz, ReplaceValue3, A0;

          end;

            suppose n1 = j;

            hence thesis by FF;

          end;

            suppose

             B1: n1 <> i & n1 <> j;

            (f,g) are_gamma-equivalent by ReplaceGamma, A0;

            hence thesis by B1, ReplaceValue, A0, A2, A1;

          end;

        end;

        hence thesis by A1, A2;

      end;

      then ( HetSet g) c< ( HetSet f) by FX;

      hence thesis by CARD_2: 48;

    end;

    theorem :: RVSUM_3:33

    

     ProdGMean: for f,g be positive non empty real-valued FinSequence st ( len f) = ( len g) & ( Product f) < ( Product g) holds ( GMean f) < ( GMean g)

    proof

      let f,g be positive non empty real-valued FinSequence;

      

       A1: ( Product f) >= 0 & ( len f) >= 1 by NAT_1: 14;

      assume ( len f) = ( len g) & ( Product f) < ( Product g);

      hence thesis by POWER: 17, A1;

    end;

    theorem :: RVSUM_3:34

    

     ExDiff: for f be positive heterogeneous non empty real-valued FinSequence holds ex i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j & (f . i) < ( Mean f) & ( Mean f) < (f . j)

    proof

      let f be positive heterogeneous non empty real-valued FinSequence;

      take i = the Element of ( MeanLess f);

      take j = the Element of ( MeanMore f);

      i in ( MeanLess f);

      then

      consider ii be Nat such that

       A1: ii = i & ii in ( dom f) & (f . ii) < ( Mean f);

      j in ( MeanMore f);

      then

      consider jj be Nat such that

       A2: jj = j & jj in ( dom f) & (f . jj) > ( Mean f);

      thus thesis by A1, A2;

    end;

    theorem :: RVSUM_3:35

    

     ReplacePositive: for f be positive heterogeneous non empty real-valued FinSequence holds for i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j & (f . i) > ( Mean f) holds ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) is positive

    proof

      let f be positive heterogeneous non empty real-valued FinSequence;

      let i,j be Nat such that

       A1: i in ( dom f) & j in ( dom f) & i <> j & (f . i) > ( Mean f);

      set a = ( Mean f);

      set b = (((f . i) + (f . j)) - ( Mean f));

      

       h2: (( Mean f) - ( Mean f)) < ((f . i) - ( Mean f)) by A1, XREAL_1: 14;

      (f . j) > 0 by A1, PosDef;

      then (((f . i) - ( Mean f)) + (f . j)) > 0 by h2;

      then

      reconsider b as positive Real;

      set g = ( Replace (f,i,j,a,b));

      for n be Nat st n in ( dom g) holds (g . n) > 0

      proof

        let n be Nat;

        assume n in ( dom g);

        then

         A2: n in ( dom f) by DinoDom;

        per cases ;

          suppose n = i;

          hence thesis by ReplaceValue3, A1;

        end;

          suppose n = j;

          hence thesis by ReplaceValue2, A1;

        end;

          suppose n <> i & n <> j;

          then (g . n) = (f . n) by A2, ReplaceValue, A1;

          hence thesis by PosDef, A2;

        end;

      end;

      hence thesis;

    end;

    theorem :: RVSUM_3:36

    

     ReplacePositive2: for f be positive heterogeneous non empty real-valued FinSequence holds for i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j & (f . j) > ( Mean f) holds ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) is positive

    proof

      let f be positive heterogeneous non empty real-valued FinSequence;

      let i,j be Nat such that

       A1: i in ( dom f) & j in ( dom f) & i <> j & (f . j) > ( Mean f);

      set a = ( Mean f);

      set b = (((f . i) + (f . j)) - ( Mean f));

      

       h2: (( Mean f) - ( Mean f)) < ((f . j) - ( Mean f)) by XREAL_1: 14, A1;

      (f . i) > 0 by A1, PosDef;

      then (((f . j) - ( Mean f)) + (f . i)) > 0 by h2;

      then

      reconsider b as positive Real;

      set g = ( Replace (f,i,j,a,b));

      for n be Nat st n in ( dom g) holds (g . n) > 0

      proof

        let n be Nat;

        assume n in ( dom g);

        then

         A2: n in ( dom f) by DinoDom;

        per cases ;

          suppose n = i;

          hence thesis by ReplaceValue3, A1;

        end;

          suppose n = j;

          hence thesis by ReplaceValue2, A1;

        end;

          suppose n <> i & n <> j;

          then (g . n) = (f . n) by A2, ReplaceValue, A1;

          hence thesis by PosDef, A2;

        end;

      end;

      hence thesis;

    end;

    theorem :: RVSUM_3:37

    for f be positive heterogeneous non empty real-valued FinSequence holds ex i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j & ex g be positive non empty real-valued FinSequence st g = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) & ( GMean f) < ( GMean g)

    proof

      let f be positive heterogeneous non empty real-valued FinSequence;

      consider j,i be Nat such that

       A1: j in ( dom f) & i in ( dom f) & j <> i & (f . j) < ( Mean f) & ( Mean f) < (f . i) by ExDiff;

      take i, j;

      thus i in ( dom f) & j in ( dom f) & i <> j by A1;

      reconsider a = ( Mean f) as positive Real;

      

       b1: (f . i) > 0 & (f . j) > 0 by A1, PosDef;

      

       h2: (( Mean f) - ( Mean f)) < ((f . i) - ( Mean f)) by A1, XREAL_1: 14;

      (f . j) > 0 by A1, PosDef;

      then (((f . i) - ( Mean f)) + (f . j)) > 0 by h2;

      then

      reconsider b = (((f . i) + (f . j)) - ( Mean f)) as positive Real;

      set g = ( Replace (f,i,j,a,b));

      

       jj: ( dom f) = ( dom g) by DinoDom;

      reconsider g as positive non empty real-valued FinSequence by ReplacePositive, A1;

      take g;

      (f . i) > (( Mean f) + 0 ) & ( Mean f) > ((f . j) + 0 ) by A1;

      then ((f . i) - ( Mean f)) > 0 & (( Mean f) - (f . j)) > 0 by XREAL_1: 20;

      then (((f . i) - ( Mean f)) * (( Mean f) - (f . j))) > 0 ;

      then (((a * b) - ((f . i) * (f . j))) + ((f . i) * (f . j))) > ( 0 + ((f . i) * (f . j))) by XREAL_1: 8;

      then ((a * b) / ((f . i) * (f . j))) > 1 by XREAL_1: 187, b1;

      then (( Product f) * ((a * b) / ((f . i) * (f . j)))) > (( Product f) * 1) by XREAL_1: 68;

      then ((( Product f) * (a * b)) / ((f . i) * (f . j))) > ( Product f) by XCMPLX_1: 74;

      then (((( Product f) * a) * b) / ((f . i) * (f . j))) > ( Product f);

      then ( Product g) > ( Product f) by A1, ProdReplace;

      hence thesis by ProdGMean, jj, FINSEQ_3: 29;

    end;

    theorem :: RVSUM_3:38

    

     BlaBla: for f be heterogeneous non empty real-valued FinSequence, i,j be Nat st i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f) holds i in ( dom f) & j in ( dom f) & i <> j & (f . i) < ( Mean f) & (f . j) > ( Mean f)

    proof

      let f be heterogeneous non empty real-valued FinSequence;

      let i,j be Nat;

      assume

       A1: i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f);

      i in ( MeanLess f) by A1;

      then

      consider ii be Nat such that

       A2: ii = i & ii in ( dom f) & (f . ii) < ( Mean f);

      j in ( MeanMore f) by A1;

      then

      consider jj be Nat such that

       A3: jj = j & jj in ( dom f) & (f . jj) > ( Mean f);

      thus thesis by A2, A3;

    end;

    theorem :: RVSUM_3:39

    

     BlaBla2: for f be heterogeneous positive non empty real-valued FinSequence, i,j be object st i in ( MeanLess f) & j in ( MeanMore f) holds i in ( dom f) & j in ( dom f) & i <> j & (f . i) < ( Mean f) & (f . j) > ( Mean f)

    proof

      let f be heterogeneous positive non empty real-valued FinSequence;

      let i,j be object;

      assume

       A1: i in ( MeanLess f) & j in ( MeanMore f);

      then

      consider ii be Nat such that

       A2: ii = i & ii in ( dom f) & (f . ii) < ( Mean f);

      consider jj be Nat such that

       A3: jj = j & jj in ( dom f) & (f . jj) > ( Mean f) by A1;

      thus thesis by A2, A3;

    end;

    theorem :: RVSUM_3:40

    for f be positive heterogeneous non empty real-valued FinSequence holds for i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j & i in ( MeanMore f) & j in ( MeanLess f) holds ex g be positive non empty real-valued FinSequence st g = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) & ( GMean f) < ( GMean g)

    proof

      let f be positive heterogeneous non empty real-valued FinSequence;

      let i,j be Nat such that

       A1: i in ( dom f) & j in ( dom f) & i <> j & i in ( MeanMore f) & j in ( MeanLess f);

      reconsider a = ( Mean f) as positive Real;

      

       b1: (f . i) > 0 & (f . j) > 0 by A1, PosDef;

      

       h1: ( Mean f) < (f . i) by A1, BlaBla2;

      then

       h2: (( Mean f) - ( Mean f)) < ((f . i) - ( Mean f)) by XREAL_1: 14;

      (f . j) > 0 by A1, PosDef;

      then (((f . i) - ( Mean f)) + (f . j)) > 0 by h2;

      then

      reconsider b = (((f . i) + (f . j)) - ( Mean f)) as positive Real;

      set g = ( Replace (f,i,j,a,b));

      

       jj: ( dom f) = ( dom g) by DinoDom;

      reconsider g as positive non empty real-valued FinSequence by ReplacePositive, A1, h1;

      take g;

      (f . i) > (( Mean f) + 0 ) & ( Mean f) > ((f . j) + 0 ) by A1, BlaBla2;

      then ((f . i) - ( Mean f)) > 0 & (( Mean f) - (f . j)) > 0 by XREAL_1: 20;

      then (((f . i) - ( Mean f)) * (( Mean f) - (f . j))) > 0 ;

      then (((a * b) - ((f . i) * (f . j))) + ((f . i) * (f . j))) > ( 0 + ((f . i) * (f . j))) by XREAL_1: 6;

      then ((a * b) / ((f . i) * (f . j))) > 1 by XREAL_1: 187, b1;

      then (( Product f) * ((a * b) / ((f . i) * (f . j)))) > (( Product f) * 1) by XREAL_1: 68;

      then ((( Product f) * (a * b)) / ((f . i) * (f . j))) > ( Product f) by XCMPLX_1: 74;

      then (((( Product f) * a) * b) / ((f . i) * (f . j))) > ( Product f);

      then ( Product g) > ( Product f) by A1, ProdReplace;

      hence thesis by ProdGMean, jj, FINSEQ_3: 29;

    end;

    theorem :: RVSUM_3:41

    

     ReplaceGMean3: for f be positive heterogeneous non empty real-valued FinSequence holds for i,j be Nat st i in ( dom f) & j in ( dom f) & i <> j & j in ( MeanMore f) & i in ( MeanLess f) holds ex g be positive non empty real-valued FinSequence st g = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) & ( GMean f) < ( GMean g)

    proof

      let f be positive heterogeneous non empty real-valued FinSequence;

      let i,j be Nat such that

       A1: i in ( dom f) & j in ( dom f) & i <> j & j in ( MeanMore f) & i in ( MeanLess f);

      reconsider a = ( Mean f) as positive Real;

      

       b1: (f . i) > 0 & (f . j) > 0 by A1, PosDef;

      

       h1: ( Mean f) < (f . j) by A1, BlaBla2;

      then

       h2: (( Mean f) - ( Mean f)) < ((f . j) - ( Mean f)) by XREAL_1: 14;

      (f . i) > 0 by A1, PosDef;

      then (((f . j) - ( Mean f)) + (f . i)) > 0 by h2;

      then

      reconsider b = (((f . i) + (f . j)) - ( Mean f)) as positive Real;

      set g = ( Replace (f,i,j,a,b));

      

       jj: ( dom f) = ( dom g) by DinoDom;

      reconsider g as positive non empty real-valued FinSequence by ReplacePositive2, A1, h1;

      take g;

      (f . j) > (( Mean f) + 0 ) & ( Mean f) > ((f . i) + 0 ) by A1, BlaBla2;

      then ((f . j) - ( Mean f)) > 0 & (( Mean f) - (f . i)) > 0 by XREAL_1: 20;

      then (((f . j) - ( Mean f)) * (( Mean f) - (f . i))) > 0 ;

      then

       k2: (((a * b) - ((f . i) * (f . j))) + ((f . i) * (f . j))) > ( 0 + ((f . i) * (f . j))) by XREAL_1: 8;

      ((a * b) / ((f . i) * (f . j))) > 1 by k2, XREAL_1: 187, b1;

      then (( Product f) * ((a * b) / ((f . i) * (f . j)))) > (( Product f) * 1) by XREAL_1: 68;

      then ((( Product f) * (a * b)) / ((f . i) * (f . j))) > ( Product f) by XCMPLX_1: 74;

      then (((( Product f) * a) * b) / ((f . i) * (f . j))) > ( Product f);

      then ( Product g) > ( Product f) by A1, ProdReplace;

      hence thesis by ProdGMean, jj, FINSEQ_3: 29;

    end;

    begin

    definition

      let f be heterogeneous positive non empty real-valued FinSequence;

      :: RVSUM_3:def10

      func Homogen f -> real-valued FinSequence means

      : HomDef: ex i,j be Nat st i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f) & it = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f))));

      existence

      proof

        set i = the Element of ( MeanLess f), j = the Element of ( MeanMore f);

        reconsider i, j as Nat;

        ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) is real-valued FinSequence;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: RVSUM_3:42

    

     DomHomogen: for f be heterogeneous positive non empty real-valued FinSequence holds ( dom ( Homogen f)) = ( dom f)

    proof

      let f be heterogeneous positive non empty real-valued FinSequence;

      consider i,j be Nat such that

       A1: i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f) & ( Homogen f) = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) by HomDef;

      thus thesis by DinoDom, A1;

    end;

    registration

      let f be heterogeneous positive non empty real-valued FinSequence;

      cluster ( Homogen f) -> non empty;

      coherence

      proof

        ( dom ( Homogen f)) = ( dom f) by DomHomogen;

        hence thesis;

      end;

    end

    registration

      let f be heterogeneous positive non empty real-valued FinSequence;

      cluster ( Homogen f) -> positive;

      coherence

      proof

        consider i,j be Nat such that

         A1: i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f) & ( Homogen f) = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) by HomDef;

        i in ( MeanLess f) by A1;

        then

        consider ii be Nat such that

         A2: ii = i & ii in ( dom f) & (f . ii) < ( Mean f);

        j in ( MeanMore f) by A1;

        then

        consider jj be Nat such that

         A3: jj = j & jj in ( dom f) & (f . jj) > ( Mean f);

        thus thesis by A1, ReplacePositive2, A2, A3;

      end;

    end

    theorem :: RVSUM_3:43

    

     HomogenHet: for f be heterogeneous positive non empty real-valued FinSequence holds ( Het ( Homogen f)) < ( Het f)

    proof

      let f be heterogeneous positive non empty real-valued FinSequence;

      consider i,j be Nat such that

       A1: i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f) & ( Homogen f) = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) by HomDef;

      

       A2: i in ( dom f) & j in ( dom f) & i <> j by A1, BlaBla;

      (f . i) <> ( Mean f) & (f . j) <> ( Mean f) by A1, BlaBla;

      hence thesis by HetMono, A1, A2;

    end;

    theorem :: RVSUM_3:44

    

     HomEqui: for f be heterogeneous positive non empty real-valued FinSequence holds (( Homogen f),f) are_gamma-equivalent

    proof

      let f be heterogeneous positive non empty real-valued FinSequence;

      consider i,j be Nat such that

       A1: i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f) & ( Homogen f) = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) by HomDef;

      i in ( dom f) & j in ( dom f) & i <> j by A1, BlaBla;

      hence thesis by A1, ReplaceGamma;

    end;

    theorem :: RVSUM_3:45

    

     HomGMean: for f be heterogeneous positive non empty real-valued FinSequence holds ( GMean ( Homogen f)) > ( GMean f)

    proof

      let f be heterogeneous positive non empty real-valued FinSequence;

      consider i,j be Nat such that

       A1: i = the Element of ( MeanLess f) & j = the Element of ( MeanMore f) & ( Homogen f) = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) by HomDef;

      i in ( dom f) & j in ( dom f) & i <> j by A1, BlaBla2;

      then

      consider g be positive non empty real-valued FinSequence such that

       J1: g = ( Replace (f,i,j,( Mean f),(((f . i) + (f . j)) - ( Mean f)))) & ( GMean f) < ( GMean g) by A1, ReplaceGMean3;

      thus thesis by J1, A1;

    end;

    begin

    theorem :: RVSUM_3:46

    

     WOWTheo: for f be heterogeneous positive non empty real-valued FinSequence holds ex g be non empty homogeneous positive real-valued FinSequence st ( GMean g) > ( GMean f) & ( Mean g) = ( Mean f)

    proof

      let f be heterogeneous positive non empty real-valued FinSequence;

      defpred P[ Nat] means ex g be positive non empty real-valued FinSequence st ( Het g) = $1 & ( Mean f) = ( Mean g) & ( GMean g) > ( GMean f) & ( Het g) < ( Het f);

      

       B1: ex k be Nat st P[k]

      proof

        reconsider g = ( Homogen f) as positive non empty real-valued FinSequence;

        take k = ( Het g);

        take g;

        (g,f) are_gamma-equivalent by HomEqui;

        hence thesis by HomogenHet, HomGMean;

      end;

      

       B2: for k be Nat st k <> 0 & P[k] holds ex n be Nat st n < k & P[n]

      proof

        let k be Nat;

        assume

         Y1: k <> 0 & P[k];

        then

        consider g be positive non empty real-valued FinSequence such that

         Y2: ( Het g) = k & ( Mean f) = ( Mean g) & ( GMean g) > ( GMean f) & ( Het g) < ( Het f);

        reconsider g as heterogeneous positive non empty real-valued FinSequence by Y1, Y2, HetHetero;

        reconsider h = ( Homogen g) as positive non empty real-valued FinSequence;

        take n = ( Het h);

        thus n < k by Y2, HomogenHet;

        thus P[n]

        proof

          ex g1 be positive non empty real-valued FinSequence st ( Het g1) = n & ( Mean f) = ( Mean g1) & ( GMean g1) > ( GMean f) & ( Het g1) < ( Het f)

          proof

            take h;

            (h,g) are_gamma-equivalent by HomEqui;

            hence thesis by Y2, HomogenHet, XXREAL_0: 2, HomGMean;

          end;

          hence thesis;

        end;

      end;

       P[ 0 ] from NAT_1:sch 7( B1, B2);

      then

      consider g be positive non empty real-valued FinSequence such that

       WW: ( Het g) = 0 & ( Mean f) = ( Mean g) & ( GMean g) > ( GMean f) & ( Het g) < ( Het f);

      g is homogeneous by WW;

      hence thesis by WW;

    end;

    theorem :: RVSUM_3:47

    for f be non empty positive real-valued FinSequence holds ( GMean f) <= ( Mean f)

    proof

      let f be non empty positive real-valued FinSequence;

      per cases ;

        suppose ( Het f) = 0 ;

        then

        reconsider ff = f as non empty homogeneous positive real-valued FinSequence;

        ( GMean ff) = ( Mean ff) by HetBase;

        hence thesis;

      end;

        suppose ( Het f) <> 0 ;

        then

        reconsider ff = f as non empty heterogeneous positive real-valued FinSequence by HetHetero;

        ex g be non empty homogeneous positive real-valued FinSequence st ( GMean g) > ( GMean ff) & ( Mean g) = ( Mean ff) by WOWTheo;

        hence thesis by HetBase;

      end;

    end;