holder_1.miz



    begin

    reserve a,b,p,q for Real;

    registration

      let x be Real;

      cluster ( right_closed_halfline x) -> non empty;

      coherence

      proof

        reconsider x as Real;

        x in { g where g be Real : x <= g };

        hence thesis by XXREAL_1: 232;

      end;

    end

    theorem :: HOLDER_1:1

    for p,q be Real st 0 < p & 0 < q holds for a be Real st 0 <= a holds ((a to_power p) * (a to_power q)) = (a to_power (p + q))

    proof

      let p,q be Real such that

       A1: 0 < p and

       A2: 0 < q;

      let a be Real such that

       A3: 0 <= a;

      now

        per cases ;

          case

           A4: a = 0 ;

          

          then ((a to_power p) * (a to_power q)) = ( 0 * ( 0 to_power q)) by A1, POWER:def 2

          .= 0 ;

          hence thesis by A1, A2, A4, POWER:def 2;

        end;

          case a <> 0 ;

          hence thesis by A3, POWER: 27;

        end;

      end;

      hence thesis;

    end;

    theorem :: HOLDER_1:2

    for p,q be Real st 0 < p & 0 < q holds for a be Real st 0 <= a holds ((a to_power p) to_power q) = (a to_power (p * q))

    proof

      let p,q be Real such that

       A1: 0 < p and

       A2: 0 < q;

      

       A3: 0 < (p * q) by A1, A2, XREAL_1: 129;

      let a be Real such that

       A4: 0 <= a;

      now

        per cases ;

          case

           A5: a = 0 ;

          

          then ((a to_power p) to_power q) = ( 0 to_power q) by A1, POWER:def 2

          .= 0 by A2, POWER:def 2;

          hence thesis by A3, A5, POWER:def 2;

        end;

          case a <> 0 ;

          hence thesis by A4, POWER: 33;

        end;

      end;

      hence thesis;

    end;

    theorem :: HOLDER_1:3

    

     Th3: for p be Real st 0 <= p holds for a,b be Real st 0 <= a & a <= b holds (a to_power p) <= (b to_power p)

    proof

      let p be Real such that

       A1: 0 <= p;

      let a,b be Real such that

       A2: 0 <= a and

       A3: a <= b;

      per cases by A1;

        suppose

         S1: 0 = p;

        (a to_power 0 ) = 1 & (b to_power 0 ) = 1 by POWER: 24;

        hence thesis by S1;

      end;

        suppose

         S2: 0 < p;

        per cases ;

          suppose a = b;

          hence thesis;

        end;

          suppose

           A4: a <> b;

          

           A5: a < b by A3, A4, XXREAL_0: 1;

          now

            per cases ;

              suppose

               A6: a = 0 ;

              then (a to_power p) = 0 by S2, POWER:def 2;

              hence thesis by A3, A4, A6, POWER: 34;

            end;

              suppose a <> 0 ;

              hence thesis by A2, A5, S2, POWER: 37;

            end;

          end;

          hence thesis;

        end;

      end;

    end;

    theorem :: HOLDER_1:4

    

     Th4: 1 < p & ((1 / p) + (1 / q)) = 1 & 0 < a & 0 < b implies (a * b) <= (((a #R p) / p) + ((b #R q) / q)) & ((a * b) = (((a #R p) / p) + ((b #R q) / q)) iff (a #R p) = (b #R q))

    proof

      assume that

       A1: 1 < p and

       A2: ((1 / p) + (1 / q)) = 1 and

       A3: 0 < a and

       A4: 0 < b;

      

       A5: 0 < (b #R q) by A4, PREPOWER: 81;

      reconsider pp = (1 / p) as Real;

      (1 - pp) <> 0 by A1, XREAL_1: 189;

      then

       A6: ((q " ) " ) <> 0 by A2;

      then ((((1 * q) + (1 * p)) / (p * q)) * (p * q)) = (1 * (p * q)) by A1, A2, XCMPLX_1: 116;

      then

       A7: (q + p) = (p * q) by A1, A6, XCMPLX_1: 6, XCMPLX_1: 87;

      then

       A8: ((q - 1) * p) = q;

      

       A9: 0 < (b #R (q - 1)) by A4, PREPOWER: 81;

       A10:

      now

        assume

         A11: (a #R p) = (b #R q);

        then

         A12: (a #R p) = ((b #R (q - 1)) #R p) by A4, A8, PREPOWER: 91;

        a = (a #R 1) by A3, PREPOWER: 72

        .= (a #R (p * (1 / p))) by A1, XCMPLX_1: 106

        .= ((a #R p) #R (1 / p)) by A3, PREPOWER: 91

        .= ((b #R (q - 1)) #R (p * (1 / p))) by A4, A12, PREPOWER: 81, PREPOWER: 91

        .= ((b #R (q - 1)) #R 1) by A1, XCMPLX_1: 106

        .= (b #R (q - 1)) by A4, PREPOWER: 72, PREPOWER: 81;

        then (a * 1) = (b #R (q - 1));

        then (a * (b #R ((1 - q) + (q - 1)))) = (b #R (q - 1)) by A4, PREPOWER: 71;

        then (a * ((b #R (1 - q)) * (b #R (q - 1)))) = (1 * (b #R (q - 1))) by A4, PREPOWER: 75;

        then

         A13: ((a * (b #R (1 - q))) * (b #R (q - 1))) = (1 * (b #R (q - 1)));

        

        thus (((a #R p) / p) + ((b #R q) / q)) = (((b #R q) * (1 / p)) + ((b #R q) / q)) by A11, XCMPLX_1: 99

        .= (((b #R q) * (1 / p)) + ((b #R q) * (1 / q))) by XCMPLX_1: 99

        .= ((b #R q) * ((1 / p) + (1 / q)))

        .= ((b #R q) * (a * (b #R (1 - q)))) by A2, A9, A13, XCMPLX_1: 5

        .= (a * ((b #R (1 - q)) * (b #R q)))

        .= (a * (b #R ((1 - q) + q))) by A4, PREPOWER: 75

        .= (a * b) by A4, PREPOWER: 72;

      end;

      

       A14: 0 < (b #R (1 - q)) by A4, PREPOWER: 81;

      then

       A15: ( 0 * (b #R (1 - q))) < (a * (b #R (1 - q))) by A3, XREAL_1: 68;

      ex h be PartFunc of REAL , REAL st ( dom h) = ( right_open_halfline 0 ) & for x be Real st x > 0 holds (h . x) = ((x #R p) / p) & h is_differentiable_in x & ( diff (h,x)) = (x #R (p - 1))

      proof

        set h = ((1 / p) (#) ( #R p));

        take h;

        ( dom ( #R p)) = ( right_open_halfline 0 ) by TAYLOR_1:def 4;

        hence

         A16: ( dom h) = ( right_open_halfline 0 ) by VALUED_1:def 5;

        now

          let x be Real such that

           A17: x > 0 ;

          x in { g where g be Real : 0 < g } by A17;

          then

           A18: x in ( right_open_halfline 0 ) by XXREAL_1: 230;

          

          hence (h . x) = ((1 / p) * (( #R p) . x)) by A16, VALUED_1:def 5

          .= ((1 / p) * (x #R p)) by A18, TAYLOR_1:def 4

          .= ((x #R p) / p) by XCMPLX_1: 99;

          

           A19: ( #R p) is_differentiable_in x by A17, TAYLOR_1: 21;

          hence h is_differentiable_in x by FDIFF_1: 15;

          

          thus ( diff (h,x)) = ((1 / p) * ( diff (( #R p),x))) by A19, FDIFF_1: 15

          .= ((1 / p) * (p * (x #R (p - 1)))) by A17, TAYLOR_1: 21

          .= (((1 / p) * p) * (x #R (p - 1)))

          .= (1 * (x #R (p - 1))) by A1, XCMPLX_1: 106

          .= (x #R (p - 1));

        end;

        hence thesis;

      end;

      then

      consider h be PartFunc of REAL , REAL such that

       A20: ( dom h) = ( right_open_halfline 0 ) and

       A21: for x be Real st x > 0 holds (h . x) = ((x #R p) / p) & h is_differentiable_in x & ( diff (h,x)) = (x #R (p - 1));

      ex g be PartFunc of REAL , REAL st ( dom g) = REAL & for x be Element of REAL holds (g . x) = ((1 / q) - x) & g is_differentiable_in x & ( diff (g,x)) = ( - 1)

      proof

        deffunc U( Real) = ( In (((1 / q) - $1), REAL ));

        defpred X[ set] means $1 in REAL ;

        consider g be PartFunc of REAL , REAL such that

         A22: for d be Element of REAL holds d in ( dom g) iff X[d] and

         A23: for d be Element of REAL st d in ( dom g) holds (g /. d) = U(d) from PARTFUN2:sch 2;

        take g;

        for x be object st x in REAL holds x in ( dom g) by A22;

        then

         A24: ( dom g) c= REAL & REAL c= ( dom g) by RELAT_1:def 18;

        then

         A25: ( dom g) = ( [#] REAL ) by XBOOLE_0:def 10;

        

         A26: for d be Element of REAL holds (g . d) = ((1 / q) - d)

        proof

          let d be Element of REAL ;

          (g /. d) = U(d) by A23, A25;

          hence thesis by A25, PARTFUN1:def 6;

        end;

        

         A27: for d be Real st d in REAL holds (g . d) = ((( - 1) * d) + (1 / q))

        proof

          let d be Real such that

           A28: d in REAL ;

          

          thus (g . d) = ((1 / q) - d) by A26, A28

          .= ((( - 1) * d) + (1 / q));

        end;

        then

         A29: g is_differentiable_on ( dom g) by A25, FDIFF_1: 23;

        for x be Element of REAL holds g is_differentiable_in x & ( diff (g,x)) = ( - 1)

        proof

          let d be Element of REAL ;

          thus g is_differentiable_in d by A25, A29, FDIFF_1: 9;

          

          thus ( diff (g,d)) = ((g `| ( dom g)) . d) by A25, A29, FDIFF_1:def 7

          .= ( - 1) by A25, A27, FDIFF_1: 23;

        end;

        hence thesis by A24, A26, XBOOLE_0:def 10;

      end;

      then

      consider g be PartFunc of REAL , REAL such that

       A30: ( dom g) = REAL and

       A31: for x be Element of REAL holds (g . x) = ((1 / q) - x) and

       A32: for x be Element of REAL holds g is_differentiable_in x & ( diff (g,x)) = ( - 1);

      set f = (h + g);

      

       A33: ( dom f) = (( right_open_halfline 0 ) /\ REAL ) by A30, A20, VALUED_1:def 1

      .= ( right_open_halfline 0 ) by XBOOLE_1: 28;

      

       A34: for x be Real st x in ( right_open_halfline 0 ) holds (f . x) = ((((x #R p) / p) + (1 / q)) - x) & f is_differentiable_in x & ( diff (f,x)) = ((x #R (p - 1)) - 1)

      proof

        let x be Real such that

         A35: x in ( right_open_halfline 0 );

        reconsider xx = x as Element of REAL by XREAL_0:def 1;

        x in { y where y be Real : 0 < y } by A35, XXREAL_1: 230;

        then

         A36: ex y be Real st x = y & 0 < y;

        then

         A37: ( diff (h,x)) = (x #R (p - 1)) by A21;

        

        thus (f . x) = ((h . x) + (g . x)) by A33, A35, VALUED_1:def 1

        .= (((x #R p) / p) + (g . xx)) by A21, A36

        .= (((x #R p) / p) + ((1 / q) - x)) by A31

        .= ((((x #R p) / p) + (1 / q)) - x);

        

         A38: g is_differentiable_in xx by A32;

        

         A39: h is_differentiable_in x by A21, A36;

        hence f is_differentiable_in x by A38, FDIFF_1: 13;

        

         A40: ( diff (g,xx)) = ( - 1) by A32;

        

        thus ( diff (f,x)) = (( diff (h,x)) + ( diff (g,x))) by A38, A39, FDIFF_1: 13

        .= ((x #R (p - 1)) - 1) by A40, A37;

      end;

      

       A41: for x be Real st 0 < x & x <> 1 holds x < (((x #R p) / p) + (1 / q))

      proof

        1 in { y where y be Real : 0 < y };

        then 1 in ( right_open_halfline 0 ) by XXREAL_1: 230;

        

        then

         A42: (f . 1) = ((((1 #R p) / p) + (1 / q)) - 1) by A34

        .= (((1 / p) + (1 / q)) - 1) by PREPOWER: 73

        .= 0 by A2;

        for x be Real st x in ( right_open_halfline 0 ) holds f is_differentiable_in x by A34;

        then

         A43: f is_differentiable_on ( right_open_halfline 0 ) by A33, FDIFF_1: 9;

        let x be Real such that

         A44: 0 < x and

         A45: x <> 1;

        x in { y where y be Real : 0 < y } by A44;

        then

         A46: x in ( right_open_halfline 0 ) by XXREAL_1: 230;

        now

          per cases by A45, XXREAL_0: 1;

            case x < 1;

            then

             A47: (1 - 1) < (1 - x) by XREAL_1: 15;

            set t = (1 - x);

            

             A48: (1 - 1) < (p - 1) by A1, XREAL_1: 14;

            now

              let z be object;

              assume z in [.x, (x + t).];

              then z in { r where r be Real : x <= r & r <= (x + t) } by RCOMP_1:def 1;

              then ex r be Real st r = z & x <= r & r <= (x + t);

              then z in { y where y be Real : 0 < y } by A44;

              hence z in ( right_open_halfline 0 ) by XXREAL_1: 230;

            end;

            then

             A49: [.x, (x + t).] c= ( right_open_halfline 0 );

            (f | ( right_open_halfline 0 )) is continuous by A43, FDIFF_1: 25;

            then

             A50: (f | [.x, (x + t).]) is continuous by A49, FCONT_1: 16;

             ].x, (x + t).[ c= [.x, (x + t).] by XXREAL_1: 25;

            then f is_differentiable_on ].x, (x + t).[ by A43, A49, FDIFF_1: 26, XBOOLE_1: 1;

            then

            consider s be Real such that

             A51: 0 < s and

             A52: s < 1 and

             A53: (f . (x + t)) = ((f . x) + (t * ( diff (f,(x + (s * t)))))) by A33, A47, A49, A50, ROLLE: 4;

            (s * t) < (1 * t) by A47, A52, XREAL_1: 68;

            then (x + (s * t)) < (x + t) by XREAL_1: 8;

            then ((x + (s * t)) to_power (p - 1)) < ((x + (s * t)) to_power 0 ) by A44, A47, A51, A48, POWER: 40;

            then ((x + (s * t)) #R (p - 1)) < ((x + (s * t)) to_power 0 ) by A44, A47, A51, POWER:def 2;

            then ((x + (s * t)) #R (p - 1)) < ((x + (s * t)) #R 0 ) by A44, A47, A51, POWER:def 2;

            then ((x + (s * t)) #R (p - 1)) < 1 by A44, A47, A51, PREPOWER: 71;

            then

             A54: (((x + (s * t)) #R (p - 1)) - 1) < (1 - 1) by XREAL_1: 14;

            (x + (s * t)) in { y where y be Real : 0 < y } by A44, A47, A51;

            then (x + (s * t)) in ( right_open_halfline 0 ) by XXREAL_1: 230;

            then ( diff (f,(x + (s * t)))) = (((x + (s * t)) #R (p - 1)) - 1) by A34;

            then (t * ( diff (f,(x + (s * t))))) < (t * 0 ) by A47, A54, XREAL_1: 68;

            then ((f . x) + (t * ( diff (f,(x + (s * t)))))) < ((f . x) + 0 ) by XREAL_1: 8;

            then 0 < ((((x #R p) / p) + (1 / q)) - x) by A34, A46, A42, A53;

            then ( 0 + x) < (((((x #R p) / p) + (1 / q)) - x) + x) by XREAL_1: 8;

            hence thesis;

          end;

            case x > 1;

            then

             A55: (1 - 1) < (x - 1) by XREAL_1: 14;

            set t = (x - 1);

            now

              let z be object;

              assume z in [.1, (1 + t).];

              then z in { r where r be Real : 1 <= r & r <= (1 + t) } by RCOMP_1:def 1;

              then ex r be Real st r = z & 1 <= r & r <= (1 + t);

              then z in { y where y be Real : 0 < y };

              hence z in ( right_open_halfline 0 ) by XXREAL_1: 230;

            end;

            then

             A56: [.1, (1 + t).] c= ( right_open_halfline 0 );

            

             A57: (1 - 1) < (p - 1) by A1, XREAL_1: 14;

            (f | ( right_open_halfline 0 )) is continuous by A43, FDIFF_1: 25;

            then

             A58: (f | [.1, (1 + t).]) is continuous by A56, FCONT_1: 16;

             ].1, (1 + t).[ c= [.1, (1 + t).] by XXREAL_1: 25;

            then f is_differentiable_on ].1, (1 + t).[ by A43, A56, FDIFF_1: 26, XBOOLE_1: 1;

            then

            consider s be Real such that

             A59: 0 < s and s < 1 and

             A60: (f . (1 + t)) = ((f . 1) + (t * ( diff (f,(1 + (s * t)))))) by A33, A55, A56, A58, ROLLE: 4;

            ( 0 * t) < (s * t) by A55, A59, XREAL_1: 68;

            then (1 + 0 ) < (1 + (s * t)) by XREAL_1: 8;

            then 1 < ((1 + (s * t)) #R (p - 1)) by A57, PREPOWER: 86;

            then

             A61: (1 - 1) < (((1 + (s * t)) #R (p - 1)) - 1) by XREAL_1: 14;

            (1 + (s * t)) in { y where y be Real : 0 < y } by A55, A59;

            then (1 + (s * t)) in ( right_open_halfline 0 ) by XXREAL_1: 230;

            then ( diff (f,(1 + (s * t)))) = (((1 + (s * t)) #R (p - 1)) - 1) by A34;

            then (t * 0 ) < (t * ( diff (f,(1 + (s * t))))) by A55, A61, XREAL_1: 68;

            then 0 < ((((x #R p) / p) + (1 / q)) - x) by A34, A46, A42, A60;

            then ( 0 + x) < (((((x #R p) / p) + (1 / q)) - x) + x) by XREAL_1: 8;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A62: (((1 - q) * p) + q) = 0 by A7;

       A63:

      now

        assume (a * b) = (((a #R p) / p) + ((b #R q) / q));

        then (a * b) = (((a #R p) / p) + ((1 / q) * (b #R q))) by XCMPLX_1: 99;

        then (a * b) = (((a #R p) * (1 / p)) + ((1 / q) * (b #R q))) by XCMPLX_1: 99;

        then (a * b) = (((a #R p) * ((b #R 0 ) / p)) + ((1 / q) * (b #R q))) by A4, PREPOWER: 71;

        then (a * b) = (((a #R p) * (((b #R ((1 - q) * p)) * (b #R q)) / p)) + ((1 / q) * (b #R q))) by A4, A62, PREPOWER: 75;

        then (a * b) = (((a #R p) * (((b #R ((1 - q) * p)) / p) * (b #R q))) + ((1 / q) * (b #R q))) by XCMPLX_1: 74;

        then (a * b) = ((((a #R p) * ((b #R ((1 - q) * p)) / p)) * (b #R q)) + ((1 / q) * (b #R q)));

        then (a * b) = (((((a #R p) * (b #R ((1 - q) * p))) / p) * (b #R q)) + ((1 / q) * (b #R q))) by XCMPLX_1: 74;

        then (a * b) = (((((a #R p) * (b #R ((1 - q) * p))) / p) + (1 / q)) * (b #R q));

        then (a * b) = (((((a #R p) * ((b #R (1 - q)) #R p)) / p) + (1 / q)) * (b #R q)) by A4, PREPOWER: 91;

        then (a * b) = (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q)) by A3, A14, PREPOWER: 78;

        then (a * (b #R ((1 - q) + q))) = (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q)) by A4, PREPOWER: 72;

        then (a * ((b #R (1 - q)) * (b #R q))) = (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q)) by A4, PREPOWER: 75;

        then ((a * (b #R (1 - q))) * (b #R q)) = (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q));

        then

         A64: (a * (b #R (1 - q))) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) by A5, XCMPLX_1: 5;

        (a * ((b #R (1 - q)) * (b #R (q - 1)))) = ((a * (b #R (1 - q))) * (b #R (q - 1)))

        .= (1 * (b #R (q - 1))) by A41, A15, A64;

        then (a * (b #R ((1 - q) + (q - 1)))) = (b #R (q - 1)) by A4, PREPOWER: 75;

        then (a * 1) = (b #R (q - 1)) by A4, PREPOWER: 71;

        hence (a #R p) = (b #R q) by A4, A8, PREPOWER: 91;

      end;

      (a * (b #R (1 - q))) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q))

      proof

        now

          per cases ;

            case (a * (b #R (1 - q))) = 1;

            hence (a * (b #R (1 - q))) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) by A2, PREPOWER: 73;

          end;

            case (a * (b #R (1 - q))) <> 1;

            hence thesis by A41, A15;

          end;

        end;

        hence thesis;

      end;

      then ((a * (b #R (1 - q))) * (b #R q)) <= (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q)) by A5, XREAL_1: 64;

      then (a * ((b #R (1 - q)) * (b #R q))) <= (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q));

      then (a * (b #R ((1 - q) + q))) <= (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q)) by A4, PREPOWER: 75;

      then (a * b) <= (((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q)) by A4, PREPOWER: 72;

      then (a * b) <= (((((a #R p) * ((b #R (1 - q)) #R p)) / p) + (1 / q)) * (b #R q)) by A3, A14, PREPOWER: 78;

      then (a * b) <= (((((a #R p) * (b #R ((1 - q) * p))) / p) + (1 / q)) * (b #R q)) by A4, PREPOWER: 91;

      then (a * b) <= (((((a #R p) * (b #R ((1 - q) * p))) / p) * (b #R q)) + ((1 / q) * (b #R q)));

      then (a * b) <= ((((a #R p) * ((b #R ((1 - q) * p)) / p)) * (b #R q)) + ((1 / q) * (b #R q))) by XCMPLX_1: 74;

      then (a * b) <= (((a #R p) * (((b #R ((1 - q) * p)) / p) * (b #R q))) + ((1 / q) * (b #R q)));

      then (a * b) <= (((a #R p) * (((b #R ((1 - q) * p)) * (b #R q)) / p)) + ((1 / q) * (b #R q))) by XCMPLX_1: 74;

      then (a * b) <= (((a #R p) * ((b #R (((1 - q) * p) + q)) / p)) + ((1 / q) * (b #R q))) by A4, PREPOWER: 75;

      then (a * b) <= (((a #R p) * (1 / p)) + ((1 / q) * (b #R q))) by A4, A7, PREPOWER: 71;

      then (a * b) <= (((a #R p) / p) + ((1 / q) * (b #R q))) by XCMPLX_1: 99;

      hence thesis by A63, A10, XCMPLX_1: 99;

    end;

    theorem :: HOLDER_1:5

    

     Th5: 1 < p & ((1 / p) + (1 / q)) = 1 & 0 <= a & 0 <= b implies (a * b) <= (((a to_power p) / p) + ((b to_power q) / q)) & ((a * b) = (((a to_power p) / p) + ((b to_power q) / q)) iff (a to_power p) = (b to_power q))

    proof

      assume that

       A1: 1 < p and

       A2: ((1 / p) + (1 / q)) = 1 and

       A3: 0 <= a and

       A4: 0 <= b;

      

       A5: 0 <= ((a to_power p) / p)

      proof

        now

          per cases by A3;

            case 0 < a;

            then 0 < (a to_power p) by POWER: 34;

            hence thesis by A1;

          end;

            case 0 = a;

            then 0 = (a to_power p) by A1, POWER:def 2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      reconsider pp = (1 / p) as Real;

      (1 / p) < 1 by A1, XREAL_1: 189;

      then

       A6: (1 - 1) < (1 - pp) by XREAL_1: 15;

      then

       A7: 0 < q by A2;

      

       A8: 0 <= ((b to_power q) / q)

      proof

        now

          per cases by A4;

            case 0 < b;

            then 0 < (b to_power q) by POWER: 34;

            hence thesis by A7;

          end;

            case 0 = b;

            then 0 = (b to_power q) by A7, POWER:def 2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      now

        per cases ;

          case

           A9: (a * b) = 0 ;

          now

            per cases by A9, XCMPLX_1: 6;

              case

               A10: a = 0 ;

               A11:

              now

                assume (a * b) = (((a to_power p) / p) + ((b to_power q) / q));

                then 0 = (( 0 / p) + ((b to_power q) / q)) by A1, A10, POWER:def 2;

                then ( 0 * q) = (((b to_power q) / q) * q);

                then 0 = (b to_power q) by A7, XCMPLX_1: 87;

                then

                 A12: 0 = ((b to_power q) to_power (1 / q)) by A2, A6, POWER:def 2;

                

                 A13: 0 = b

                proof

                  assume

                   A14: b <> 0 ;

                  then 0 = (b to_power (q * (1 / q))) by A4, A12, POWER: 33;

                  then 0 = (b to_power 1) by A7, XCMPLX_1: 106;

                  hence contradiction by A14, POWER: 25;

                end;

                

                thus (a to_power p) = 0 by A1, A10, POWER:def 2

                .= (b to_power q) by A7, A13, POWER:def 2;

              end;

              now

                assume (a to_power p) = (b to_power q);

                

                then

                 A15: ((b to_power q) / q) = ( 0 / q) by A1, A10, POWER:def 2

                .= 0 ;

                ((a to_power p) / p) = ( 0 / p) by A1, A10, POWER:def 2

                .= 0 ;

                hence (a * b) = (((a to_power p) / p) + ((b to_power q) / q)) by A9, A15;

              end;

              hence (a * b) = (((a to_power p) / p) + ((b to_power q) / q)) iff (a to_power p) = (b to_power q) by A11;

            end;

              case

               A16: b = 0 ;

              

               A17: (1 / p) > 0 by A1, XREAL_1: 139;

               A18:

              now

                assume (a * b) = (((a to_power p) / p) + ((b to_power q) / q));

                then 0 = (( 0 / q) + ((a to_power p) / p)) by A7, A16, POWER:def 2;

                then ( 0 * p) = (((a to_power p) / p) * p);

                then 0 = (a to_power p) by A1, XCMPLX_1: 87;

                then

                 A19: 0 = ((a to_power p) to_power (1 / p)) by A17, POWER:def 2;

                

                 A20: 0 = a

                proof

                  assume

                   A21: a <> 0 ;

                  then 0 = (a to_power (p * (1 / p))) by A3, A19, POWER: 33;

                  then 0 = (a to_power 1) by A1, XCMPLX_1: 106;

                  hence contradiction by A21, POWER: 25;

                end;

                

                thus (b to_power q) = 0 by A7, A16, POWER:def 2

                .= (a to_power p) by A1, A20, POWER:def 2;

              end;

              now

                assume (a to_power p) = (b to_power q);

                

                then

                 A22: ((a to_power p) / p) = ( 0 / p) by A7, A16, POWER:def 2

                .= 0 ;

                ((b to_power q) / q) = ( 0 / q) by A7, A16, POWER:def 2

                .= 0 ;

                hence (a * b) = (((a to_power p) / p) + ((b to_power q) / q)) by A9, A22;

              end;

              hence (a * b) = (((a to_power p) / p) + ((b to_power q) / q)) iff (a to_power p) = (b to_power q) by A18;

            end;

          end;

          hence thesis by A5, A8;

        end;

          case

           A23: (a * b) <> 0 ;

          then

           A24: a <> 0 ;

          

           A25: b <> 0 by A23;

          then (a * b) = (((a #R p) / p) + ((b #R q) / q)) iff (a #R p) = (b #R q) by A1, A2, A3, A4, A24, Th4;

          then

           A26: (a * b) = (((a to_power p) / p) + ((b #R q) / q)) iff (a to_power p) = (b #R q) by A3, A24, POWER:def 2;

          (a * b) <= (((a #R p) / p) + ((b #R q) / q)) by A1, A2, A3, A4, A24, A25, Th4;

          then (a * b) <= (((a to_power p) / p) + ((b #R q) / q)) by A3, A24, POWER:def 2;

          hence thesis by A4, A25, A26, POWER:def 2;

        end;

      end;

      hence thesis;

    end;

    

     Lm1: for a be Real_Sequence st for n be Nat holds 0 <= (a . n) holds for n be Nat holds (a . n) <= (( Partial_Sums a) . n)

    proof

      let a be Real_Sequence such that

       A1: for n be Nat holds 0 <= (a . n);

      defpred P[ Nat] means (a . $1) <= (( Partial_Sums a) . $1);

      

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

      proof

        let n be Nat;

        assume P[n];

        then

         A3: (( Partial_Sums a) . (n + 1)) = ((( Partial_Sums a) . n) + (a . (n + 1))) & ((a . n) + (a . (n + 1))) <= ((( Partial_Sums a) . n) + (a . (n + 1))) by SERIES_1:def 1, XREAL_1: 6;

         0 <= (a . n) by A1;

        then ( 0 + (a . (n + 1))) <= ((a . n) + (a . (n + 1))) by XREAL_1: 6;

        hence thesis by A3, XXREAL_0: 2;

      end;

      

       A4: P[ 0 ] by SERIES_1:def 1;

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

      hence thesis;

    end;

    

     Lm2: for a be Real_Sequence st for n be Nat holds 0 <= (a . n) holds for n be Nat holds 0 <= (( Partial_Sums a) . n)

    proof

      let a be Real_Sequence such that

       A1: for n be Nat holds 0 <= (a . n);

      let n be Nat;

      (a . n) <= (( Partial_Sums a) . n) by A1, Lm1;

      hence thesis by A1;

    end;

    

     Lm3: for a be Real_Sequence st for n be Nat holds 0 <= (a . n) holds for n be Nat st (( Partial_Sums a) . n) = 0 holds for k be Nat st k <= n holds (a . k) = 0

    proof

      let a be Real_Sequence such that

       A1: for n be Nat holds 0 <= (a . n);

      let n be Nat such that

       A2: (( Partial_Sums a) . n) = 0 ;

      now

        

         A3: ( Partial_Sums a) is non-decreasing by A1, SERIES_1: 16;

        let k be Nat;

        assume k <= n;

        then

         A4: (( Partial_Sums a) . k) <= (( Partial_Sums a) . n) by A3, SEQM_3: 6;

        (a . k) <= (( Partial_Sums a) . k) by A1, Lm1;

        hence (a . k) = 0 by A1, A2, A4;

      end;

      hence thesis;

    end;

    

     Lm4: for a be Real_Sequence holds for n be Nat st for k be Nat st k <= n holds (a . k) = 0 holds (( Partial_Sums a) . n) = 0

    proof

      let a be Real_Sequence;

      defpred P[ Nat] means (for k be Nat st k <= $1 holds (a . k) = 0 ) implies (( Partial_Sums a) . $1) = 0 ;

      

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

      proof

        let n be Nat such that

         A2: P[n];

        now

          assume

           A3: for k be Nat st k <= (n + 1) holds (a . k) = 0 ;

           A4:

          now

            

             A5: n <= (n + 1) by NAT_1: 11;

            let k be Nat;

            assume k <= n;

            hence (a . k) = 0 by A3, A5, XXREAL_0: 2;

          end;

          

          thus (( Partial_Sums a) . (n + 1)) = ((( Partial_Sums a) . n) + (a . (n + 1))) by SERIES_1:def 1

          .= 0 by A2, A3, A4;

        end;

        hence thesis;

      end;

      

       A6: P[ 0 ]

      proof

        assume for k be Nat st k <= 0 holds (a . k) = 0 ;

        then (a . 0 ) = 0 ;

        hence thesis by SERIES_1:def 1;

      end;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A6, A1);

    end;

    begin

    theorem :: HOLDER_1:6

    

     Th6: for p,q be Real st 1 < p & ((1 / p) + (1 / q)) = 1 holds for a,b,ap,bq,ab be Real_Sequence st (for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bq . n) = ( |.(b . n).| to_power q) & (ab . n) = |.((a . n) * (b . n)).|) holds for n be Nat holds (( Partial_Sums ab) . n) <= (((( Partial_Sums ap) . n) to_power (1 / p)) * ((( Partial_Sums bq) . n) to_power (1 / q)))

    proof

      let p,q be Real such that

       A1: 1 < p and

       A2: ((1 / p) + (1 / q)) = 1;

      reconsider pp = (1 / p) as Real;

      let a,b,ap,bq,ab be Real_Sequence such that

       A3: for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bq . n) = ( |.(b . n).| to_power q) & (ab . n) = |.((a . n) * (b . n)).|;

      let n be Nat;

      set B = (( Partial_Sums bq) . n);

      (1 / p) < 1 by A1, XREAL_1: 189;

      then

       A4: (1 - 1) < (1 - pp) by XREAL_1: 15;

      then

       A5: 0 < q by A2;

      

       A6: for n be Nat holds 0 <= (bq . n)

      proof

        let n be Nat;

        

         A7: (bq . n) = ( |.(b . n).| to_power q) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(b . n).| = 0 ;

            hence thesis by A5, A7, POWER:def 2;

          end;

            case |.(b . n).| > 0 ;

            hence thesis by A7, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      then

       A8: 0 <= B by Lm2;

      set A = (( Partial_Sums ap) . n);

      

       A9: for n be Nat holds 0 <= (ap . n)

      proof

        let n be Nat;

        

         A10: (ap . n) = ( |.(a . n).| to_power p) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(a . n).| = 0 ;

            hence thesis by A1, A10, POWER:def 2;

          end;

            case |.(a . n).| > 0 ;

            hence thesis by A10, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      then

       A11: 0 <= A by Lm2;

      set Bq = (B to_power (1 / q));

      set Ap = (A to_power (1 / p));

      

       A12: (1 / p) > 0 by A1, XREAL_1: 139;

      now

        per cases ;

          case

           A13: (A * B) = 0 ;

          

           A14: 0 <= Ap

          proof

            now

              per cases by A9, Lm2;

                case 0 < A;

                hence thesis by POWER: 34;

              end;

                case 0 = A;

                hence thesis by A12, POWER:def 2;

              end;

            end;

            hence thesis;

          end;

           0 <= Bq

          proof

            now

              per cases by A6, Lm2;

                case 0 < B;

                hence thesis by POWER: 34;

              end;

                case 0 = B;

                hence thesis by A2, A4, POWER:def 2;

              end;

            end;

            hence thesis;

          end;

          then

           A15: 0 <= (Ap * Bq) by A14;

          now

            per cases by A13, XCMPLX_1: 6;

              case

               A16: A = 0 ;

              

               A17: for k be Nat st k <= n holds (a . k) = 0

              proof

                let k be Nat;

                assume k <= n;

                then (ap . k) = 0 by A9, A16, Lm3;

                then

                 A18: ( |.(a . k).| to_power p) = 0 by A3;

                 |.(a . k).| = 0

                proof

                  assume |.(a . k).| <> 0 ;

                  then |.(a . k).| > 0 by COMPLEX1: 46;

                  hence contradiction by A18, POWER: 34;

                end;

                hence thesis by ABSVALUE: 2;

              end;

              for k be Nat st k <= n holds (ab . k) = 0

              proof

                let k be Nat such that

                 A19: k <= n;

                

                thus (ab . k) = |.((a . k) * (b . k)).| by A3

                .= |.( 0 * (b . k)).| by A17, A19

                .= 0 by ABSVALUE: 2;

              end;

              hence thesis by A15, Lm4;

            end;

              case

               A20: B = 0 ;

              

               A21: for k be Nat st k <= n holds (b . k) = 0

              proof

                let k be Nat;

                assume k <= n;

                then (bq . k) = 0 by A6, A20, Lm3;

                then

                 A22: ( |.(b . k).| to_power q) = 0 by A3;

                 |.(b . k).| = 0

                proof

                  assume |.(b . k).| <> 0 ;

                  then |.(b . k).| > 0 by COMPLEX1: 46;

                  hence contradiction by A22, POWER: 34;

                end;

                hence thesis by ABSVALUE: 2;

              end;

              for k be Nat st k <= n holds (ab . k) = 0

              proof

                let k be Nat such that

                 A23: k <= n;

                

                thus (ab . k) = |.((a . k) * (b . k)).| by A3

                .= |.((a . k) * 0 ).| by A21, A23

                .= 0 by ABSVALUE: 2;

              end;

              hence thesis by A15, Lm4;

            end;

          end;

          hence thesis;

        end;

          case

           A24: (A * B) <> 0 ;

          deffunc G( Nat) = ( |.(b . $1).| / Bq);

          consider y be Real_Sequence such that

           A25: for n be Nat holds (y . n) = G(n) from SEQ_1:sch 1;

          

           A26: B <> 0 by A24;

          then

           A27: Bq > 0 by A8, POWER: 34;

          

           A28: for n be Nat holds 0 <= (y . n)

          proof

            let n be Nat;

             0 <= |.(b . n).| by COMPLEX1: 46;

            then 0 <= ( |.(b . n).| / Bq) by A27;

            hence thesis by A25;

          end;

          deffunc F( Nat) = ( |.(a . $1).| / Ap);

          consider x be Real_Sequence such that

           A29: for n be Nat holds (x . n) = F(n) from SEQ_1:sch 1;

          

           A30: for n be Nat holds (((1 / (Ap * Bq)) (#) ab) . n) = ((x . n) * (y . n))

          proof

            let n be Nat;

            (x . n) = ( |.(a . n).| / Ap) & (y . n) = ( |.(b . n).| / Bq) by A29, A25;

            

            hence ((x . n) * (y . n)) = (( |.(a . n).| * |.(b . n).|) / (Ap * Bq)) by XCMPLX_1: 76

            .= ( |.((a . n) * (b . n)).| / (Ap * Bq)) by COMPLEX1: 65

            .= ((ab . n) / (Ap * Bq)) by A3

            .= ((1 / (Ap * Bq)) * (ab . n)) by XCMPLX_1: 99

            .= (((1 / (Ap * Bq)) (#) ab) . n) by SEQ_1: 9;

          end;

          

           A31: (( Partial_Sums ((1 / (Ap * Bq)) (#) ab)) . n) = (((1 / (Ap * Bq)) (#) ( Partial_Sums ab)) . n) by SERIES_1: 9

          .= ((1 / (Ap * Bq)) * (( Partial_Sums ab) . n)) by SEQ_1: 9;

          

           A32: A <> 0 by A24;

          then

           A33: Ap > 0 by A11, POWER: 34;

          then

           A34: (Ap * Bq) > 0 by A27, XREAL_1: 129;

          

           A35: for n be Nat holds ((((1 / p) (#) ((1 / A) (#) ap)) + ((1 / q) (#) ((1 / B) (#) bq))) . n) = ((((x . n) to_power p) / p) + (((y . n) to_power q) / q))

          proof

            let n be Nat;

            

             A36: (( |.(a . n).| / Ap) to_power p) = (( |.(a . n).| to_power p) / (Ap to_power p))

            proof

              now

                per cases ;

                  case

                   A37: |.(a . n).| = 0 ;

                  

                  hence (( |.(a . n).| / Ap) to_power p) = ( 0 / (Ap to_power p)) by A1, POWER:def 2

                  .= (( |.(a . n).| to_power p) / (Ap to_power p)) by A1, A37, POWER:def 2;

                end;

                  case |.(a . n).| <> 0 ;

                  then |.(a . n).| > 0 by COMPLEX1: 46;

                  hence thesis by A33, POWER: 31;

                end;

              end;

              hence thesis;

            end;

            

             A38: (( |.(b . n).| / Bq) to_power q) = (( |.(b . n).| to_power q) / (Bq to_power q))

            proof

              now

                per cases ;

                  case

                   A39: |.(b . n).| = 0 ;

                  

                  hence (( |.(b . n).| / Bq) to_power q) = ( 0 / (Bq to_power q)) by A5, POWER:def 2

                  .= (( |.(b . n).| to_power q) / (Bq to_power q)) by A5, A39, POWER:def 2;

                end;

                  case |.(b . n).| <> 0 ;

                  then |.(b . n).| > 0 by COMPLEX1: 46;

                  hence thesis by A27, POWER: 31;

                end;

              end;

              hence thesis;

            end;

            (y . n) = ( |.(b . n).| / Bq) by A25;

            

            then

             A40: (((y . n) to_power q) / q) = (((bq . n) / (Bq to_power q)) / q) by A3, A38

            .= (((bq . n) / (B to_power ((1 / q) * q))) / q) by A8, A26, POWER: 33

            .= (((bq . n) / (B to_power 1)) / q) by A5, XCMPLX_1: 87

            .= (((bq . n) / B) / q) by POWER: 25

            .= ((1 / q) * ((bq . n) / B)) by XCMPLX_1: 99

            .= ((1 / q) * ((1 / B) * (bq . n))) by XCMPLX_1: 99

            .= ((1 / q) * (((1 / B) (#) bq) . n)) by SEQ_1: 9

            .= (((1 / q) (#) ((1 / B) (#) bq)) . n) by SEQ_1: 9;

            (x . n) = ( |.(a . n).| / Ap) by A29;

            

            then (((x . n) to_power p) / p) = (((ap . n) / (Ap to_power p)) / p) by A3, A36

            .= (((ap . n) / (A to_power ((1 / p) * p))) / p) by A11, A32, POWER: 33

            .= (((ap . n) / (A to_power 1)) / p) by A1, XCMPLX_1: 87

            .= (((ap . n) / A) / p) by POWER: 25

            .= ((1 / p) * ((ap . n) / A)) by XCMPLX_1: 99

            .= ((1 / p) * ((1 / A) * (ap . n))) by XCMPLX_1: 99

            .= ((1 / p) * (((1 / A) (#) ap) . n)) by SEQ_1: 9

            .= (((1 / p) (#) ((1 / A) (#) ap)) . n) by SEQ_1: 9;

            hence thesis by A40, SEQ_1: 7;

          end;

          

           A41: for n be Nat holds 0 <= (x . n)

          proof

            let n be Nat;

             0 <= |.(a . n).| by COMPLEX1: 46;

            then 0 <= ( |.(a . n).| / Ap) by A33;

            hence thesis by A29;

          end;

          

           A42: for n be Nat holds ((x . n) * (y . n)) <= ((((x . n) to_power p) / p) + (((y . n) to_power q) / q)) & (((x . n) * (y . n)) = ((((x . n) to_power p) / p) + (((y . n) to_power q) / q)) iff ((x . n) to_power p) = ((y . n) to_power q))

          proof

            let n be Nat;

             0 <= (x . n) & 0 <= (y . n) by A41, A28;

            hence thesis by A1, A2, Th5;

          end;

          for n be Nat holds (((1 / (Ap * Bq)) (#) ab) . n) <= ((((1 / p) (#) ((1 / A) (#) ap)) + ((1 / q) (#) ((1 / B) (#) bq))) . n)

          proof

            let n be Nat;

            ((x . n) * (y . n)) <= ((((x . n) to_power p) / p) + (((y . n) to_power q) / q)) & ((((1 / p) (#) ((1 / A) (#) ap)) + ((1 / q) (#) ((1 / B) (#) bq))) . n) = ((((x . n) to_power p) / p) + (((y . n) to_power q) / q)) by A42, A35;

            hence thesis by A30;

          end;

          then

           A43: (( Partial_Sums ((1 / (Ap * Bq)) (#) ab)) . n) <= (( Partial_Sums (((1 / p) (#) ((1 / A) (#) ap)) + ((1 / q) (#) ((1 / B) (#) bq)))) . n) by SERIES_1: 14;

          (( Partial_Sums (((1 / p) (#) ((1 / A) (#) ap)) + ((1 / q) (#) ((1 / B) (#) bq)))) . n) = ((( Partial_Sums ((1 / p) (#) ((1 / A) (#) ap))) + ( Partial_Sums ((1 / q) (#) ((1 / B) (#) bq)))) . n) by SERIES_1: 5

          .= ((( Partial_Sums ((1 / p) (#) ((1 / A) (#) ap))) . n) + (( Partial_Sums ((1 / q) (#) ((1 / B) (#) bq))) . n)) by SEQ_1: 7

          .= ((((1 / p) (#) ( Partial_Sums ((1 / A) (#) ap))) . n) + (( Partial_Sums ((1 / q) (#) ((1 / B) (#) bq))) . n)) by SERIES_1: 9

          .= (((1 / p) * (( Partial_Sums ((1 / A) (#) ap)) . n)) + (( Partial_Sums ((1 / q) (#) ((1 / B) (#) bq))) . n)) by SEQ_1: 9

          .= (((1 / p) * (((1 / A) (#) ( Partial_Sums ap)) . n)) + (( Partial_Sums ((1 / q) (#) ((1 / B) (#) bq))) . n)) by SERIES_1: 9

          .= (((1 / p) * ((1 / A) * (( Partial_Sums ap) . n))) + (( Partial_Sums ((1 / q) (#) ((1 / B) (#) bq))) . n)) by SEQ_1: 9

          .= (((1 / p) * ((1 / A) * (( Partial_Sums ap) . n))) + (((1 / q) (#) ( Partial_Sums ((1 / B) (#) bq))) . n)) by SERIES_1: 9

          .= (((1 / p) * ((1 / A) * (( Partial_Sums ap) . n))) + ((1 / q) * (( Partial_Sums ((1 / B) (#) bq)) . n))) by SEQ_1: 9

          .= (((1 / p) * ((1 / A) * (( Partial_Sums ap) . n))) + ((1 / q) * (((1 / B) (#) ( Partial_Sums bq)) . n))) by SERIES_1: 9

          .= (((1 / p) * ((1 / A) * (( Partial_Sums ap) . n))) + ((1 / q) * ((1 / B) * (( Partial_Sums bq) . n)))) by SEQ_1: 9

          .= (((1 / p) * 1) + ((1 / q) * ((1 / B) * B))) by A32, XCMPLX_1: 87

          .= (((1 / p) * 1) + ((1 / q) * 1)) by A26, XCMPLX_1: 87

          .= 1 by A2;

          then ((( Partial_Sums ab) . n) / (Ap * Bq)) <= 1 by A43, A31, XCMPLX_1: 99;

          hence thesis by A34, XREAL_1: 187;

        end;

      end;

      hence thesis;

    end;

    theorem :: HOLDER_1:7

    

     Th7: for p be Real st 1 < p holds for a,b,ap,bp,ab be Real_Sequence st (for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bp . n) = ( |.(b . n).| to_power p) & (ab . n) = ( |.((a . n) + (b . n)).| to_power p)) holds for n be Nat holds ((( Partial_Sums ab) . n) to_power (1 / p)) <= (((( Partial_Sums ap) . n) to_power (1 / p)) + ((( Partial_Sums bp) . n) to_power (1 / p)))

    proof

      let p be Real such that

       A1: 1 < p;

      

       A2: (1 / p) > 0 by A1, XREAL_1: 139;

      let a,b,ap,bp,ab be Real_Sequence such that

       A3: for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bp . n) = ( |.(b . n).| to_power p) & (ab . n) = ( |.((a . n) + (b . n)).| to_power p);

      

       A4: for n be Nat holds 0 <= (ap . n)

      proof

        let n be Nat;

        

         A5: (ap . n) = ( |.(a . n).| to_power p) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(a . n).| = 0 ;

            hence thesis by A1, A5, POWER:def 2;

          end;

            case |.(a . n).| > 0 ;

            hence thesis by A5, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      

       A6: for n be Nat holds 0 <= (bp . n)

      proof

        let n be Nat;

        

         A7: (bp . n) = ( |.(b . n).| to_power p) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(b . n).| = 0 ;

            hence thesis by A1, A7, POWER:def 2;

          end;

            case |.(b . n).| > 0 ;

            hence thesis by A7, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      deffunc F( Nat) = ( |.((a . $1) + (b . $1)).| to_power (p - 1));

      consider x be Real_Sequence such that

       A8: for n be Nat holds (x . n) = F(n) from SEQ_1:sch 1;

      

       A9: (1 - 1) < (p - 1) by A1, XREAL_1: 14;

      

       A10: for n be Nat holds 0 <= (x . n)

      proof

        let n be Nat;

        

         A11: (x . n) = ( |.((a . n) + (b . n)).| to_power (p - 1)) by A8;

        now

          per cases by COMPLEX1: 46;

            case |.((a . n) + (b . n)).| = 0 ;

            hence thesis by A9, A11, POWER:def 2;

          end;

            case |.((a . n) + (b . n)).| > 0 ;

            hence thesis by A11, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      

       A12: for n be Nat holds ((x (#) ( abs b)) . n) = |.((b . n) * (x . n)).|

      proof

        let n be Nat;

         0 <= (x . n) by A10;

        then

         A13: |.(x . n).| = (x . n) by ABSVALUE:def 1;

        

        thus ((x (#) ( abs b)) . n) = ((x . n) * (( abs b) . n)) by SEQ_1: 8

        .= ((x . n) * |.(b . n).|) by SEQ_1: 12

        .= |.((b . n) * (x . n)).| by A13, COMPLEX1: 65;

      end;

      reconsider pp = (1 / p) as Real;

      reconsider qq = (1 - pp) as Real;

      reconsider q = (1 / qq) as Real;

      

       A14: qq = (1 / q) by XCMPLX_1: 56;

      then

       A15: ((1 / p) + (1 / q)) = 1;

      (1 / p) < 1 by A1, XREAL_1: 189;

      then

       A16: (1 - 1) < (1 - pp) by XREAL_1: 15;

      then

       A17: q <> 0 by A14;

      then ((((1 * q) + (1 * p)) / (p * q)) * (p * q)) = (1 * (p * q)) by A1, A15, XCMPLX_1: 116;

      then

       A18: (q + p) = (p * q) by A1, A17, XCMPLX_1: 6, XCMPLX_1: 87;

      

       A19: for n be Nat holds (ab . n) = ((x . n) * |.((a . n) + (b . n)).|)

      proof

        let n be Nat;

        now

          per cases ;

            case

             A20: |.((a . n) + (b . n)).| = 0 ;

            

            thus (ab . n) = ( |.((a . n) + (b . n)).| to_power p) by A3

            .= ((x . n) * |.((a . n) + (b . n)).|) by A1, A20, POWER:def 2;

          end;

            case

             A21: |.((a . n) + (b . n)).| <> 0 ;

            

             A22: 0 <= |.((a . n) + (b . n)).| by COMPLEX1: 46;

            

            thus (ab . n) = ( |.((a . n) + (b . n)).| to_power ((p - 1) + 1)) by A3

            .= (( |.((a . n) + (b . n)).| to_power (p - 1)) * ( |.((a . n) + (b . n)).| to_power 1)) by A21, A22, POWER: 27

            .= (( |.((a . n) + (b . n)).| to_power (p - 1)) * |.((a . n) + (b . n)).|) by POWER: 25

            .= ((x . n) * |.((a . n) + (b . n)).|) by A8;

          end;

        end;

        hence thesis;

      end;

      

       A23: for n be Nat holds (ab . n) <= (((x (#) ( abs a)) + (x (#) ( abs b))) . n)

      proof

        let n be Nat;

        

         A24: ((x . n) * ( |.(a . n).| + |.(b . n).|)) = (((x . n) * |.(a . n).|) + ((x . n) * |.(b . n).|))

        .= (((x . n) * (( abs a) . n)) + ((x . n) * |.(b . n).|)) by SEQ_1: 12

        .= (((x . n) * (( abs a) . n)) + ((x . n) * (( abs b) . n))) by SEQ_1: 12

        .= (((x (#) ( abs a)) . n) + ((x . n) * (( abs b) . n))) by SEQ_1: 8

        .= (((x (#) ( abs a)) . n) + ((x (#) ( abs b)) . n)) by SEQ_1: 8

        .= (((x (#) ( abs a)) + (x (#) ( abs b))) . n) by SEQ_1: 7;

         0 <= (x . n) & (ab . n) = ((x . n) * |.((a . n) + (b . n)).|) by A10, A19;

        hence thesis by A24, COMPLEX1: 56, XREAL_1: 64;

      end;

      

       A25: 0 < q by A16, A14;

      

       A26: for n be Nat holds ( |.(x . n).| to_power q) = (ab . n)

      proof

        let n be Nat;

         0 <= (x . n) by A10;

        then |.(x . n).| = (x . n) by ABSVALUE:def 1;

        then

         A27: ( |.(x . n).| to_power q) = (( |.((a . n) + (b . n)).| to_power (p - 1)) to_power q) by A8;

        now

          per cases ;

            case

             A28: |.((a . n) + (b . n)).| = 0 ;

            

            then

             A29: (ab . n) = ( 0 to_power p) by A3

            .= 0 by A1, POWER:def 2;

            ( |.(x . n).| to_power q) = ( 0 to_power q) by A9, A27, A28, POWER:def 2

            .= 0 by A25, POWER:def 2;

            hence thesis by A29;

          end;

            case |.((a . n) + (b . n)).| <> 0 ;

            then 0 < |.((a . n) + (b . n)).| by COMPLEX1: 46;

            

            hence ( |.(x . n).| to_power q) = ( |.((a . n) + (b . n)).| to_power ((p - 1) * q)) by A27, POWER: 33

            .= (ab . n) by A3, A18;

          end;

        end;

        hence thesis;

      end;

      

       A30: for n be Nat holds ((x (#) ( abs a)) . n) = |.((a . n) * (x . n)).|

      proof

        let n be Nat;

         0 <= (x . n) by A10;

        then

         A31: |.(x . n).| = (x . n) by ABSVALUE:def 1;

        

        thus ((x (#) ( abs a)) . n) = ((x . n) * (( abs a) . n)) by SEQ_1: 8

        .= ((x . n) * |.(a . n).|) by SEQ_1: 12

        .= |.((a . n) * (x . n)).| by A31, COMPLEX1: 65;

      end;

      

       A32: for n be Nat holds (( Partial_Sums ab) . n) <= ((((( Partial_Sums ap) . n) to_power (1 / p)) + ((( Partial_Sums bp) . n) to_power (1 / p))) * ((( Partial_Sums ab) . n) to_power (1 / q)))

      proof

        let n be Nat;

        

         A33: (( Partial_Sums ((x (#) ( abs a)) + (x (#) ( abs b)))) . n) = ((( Partial_Sums (x (#) ( abs a))) + ( Partial_Sums (x (#) ( abs b)))) . n) by SERIES_1: 5

        .= ((( Partial_Sums (x (#) ( abs a))) . n) + (( Partial_Sums (x (#) ( abs b))) . n)) by SEQ_1: 7;

        (( Partial_Sums (x (#) ( abs a))) . n) <= (((( Partial_Sums ap) . n) to_power (1 / p)) * ((( Partial_Sums ab) . n) to_power (1 / q))) & (( Partial_Sums (x (#) ( abs b))) . n) <= (((( Partial_Sums bp) . n) to_power (1 / p)) * ((( Partial_Sums ab) . n) to_power (1 / q))) by A1, A3, A15, A30, A12, A26, Th6;

        then

         A34: ((( Partial_Sums (x (#) ( abs a))) . n) + (( Partial_Sums (x (#) ( abs b))) . n)) <= ((((( Partial_Sums ap) . n) to_power (1 / p)) * ((( Partial_Sums ab) . n) to_power (1 / q))) + (((( Partial_Sums bp) . n) to_power (1 / p)) * ((( Partial_Sums ab) . n) to_power (1 / q)))) by XREAL_1: 7;

        (( Partial_Sums ab) . n) <= (( Partial_Sums ((x (#) ( abs a)) + (x (#) ( abs b)))) . n) by A23, SERIES_1: 14;

        hence thesis by A33, A34, XXREAL_0: 2;

      end;

      

       A35: for n be Nat holds 0 <= (ab . n)

      proof

        let n be Nat;

         0 <= |.((a . n) + (b . n)).| by COMPLEX1: 46;

        then

         A36: ( 0 to_power p) <= ( |.((a . n) + (b . n)).| to_power p) by A1, Th3;

        (ab . n) = ( |.((a . n) + (b . n)).| to_power p) by A3;

        hence thesis by A1, A36, POWER:def 2;

      end;

      now

        let n be Nat;

        set A = (( Partial_Sums ab) . n);

        set C = (((( Partial_Sums ap) . n) to_power (1 / p)) + ((( Partial_Sums bp) . n) to_power (1 / p)));

        set D = (A to_power (1 / q));

        

         A37: 0 <= A by A35, Lm2;

         0 <= (( Partial_Sums bp) . n) by A6, Lm2;

        then ( 0 to_power (1 / p)) <= ((( Partial_Sums bp) . n) to_power (1 / p)) by A2, Th3;

        then

         A38: 0 <= ((( Partial_Sums bp) . n) to_power (1 / p)) by A2, POWER:def 2;

         0 <= (( Partial_Sums ap) . n) by A4, Lm2;

        then ( 0 to_power (1 / p)) <= ((( Partial_Sums ap) . n) to_power (1 / p)) by A2, Th3;

        then 0 <= ((( Partial_Sums ap) . n) to_power (1 / p)) by A2, POWER:def 2;

        then

         A39: ( 0 + 0 ) <= (((( Partial_Sums ap) . n) to_power (1 / p)) + ((( Partial_Sums bp) . n) to_power (1 / p))) by A38;

        now

          per cases ;

            case A = 0 ;

            hence (A to_power (1 / p)) <= C by A2, A39, POWER:def 2;

          end;

            case

             A40: A <> 0 ;

            set B = (1 / D);

            

             A41: 0 < D by A37, A40, POWER: 34;

            then

             A42: 0 < B by XREAL_1: 139;

            

             A43: ((C * D) * B) = (C * (D * B))

            .= (C * 1) by A41, XCMPLX_1: 87

            .= C;

            (A * B) = (A / D) by XCMPLX_1: 99

            .= ((A to_power 1) / D) by POWER: 25

            .= (A to_power (1 - (1 / q))) by A37, A40, POWER: 29

            .= (A to_power (1 / p)) by A14;

            hence (A to_power (1 / p)) <= (((( Partial_Sums ap) . n) to_power (1 / p)) + ((( Partial_Sums bp) . n) to_power (1 / p))) by A32, A42, A43, XREAL_1: 64;

          end;

        end;

        hence ((( Partial_Sums ab) . n) to_power (1 / p)) <= (((( Partial_Sums ap) . n) to_power (1 / p)) + ((( Partial_Sums bp) . n) to_power (1 / p)));

      end;

      hence thesis;

    end;

    theorem :: HOLDER_1:8

    

     Th8: for a,b be Real_Sequence st (for n be Nat holds (a . n) <= (b . n)) & b is convergent & a is non-decreasing holds a is convergent & ( lim a) <= ( lim b)

    proof

      let a,b be Real_Sequence such that

       A1: for n be Nat holds (a . n) <= (b . n) and

       A2: b is convergent and

       A3: a is non-decreasing;

      

       A4: b is bounded by A2;

      

       A5: a is bounded_above

      proof

        consider r be Real such that

         A6: for n be Nat holds (b . n) < r by A4, SEQ_2:def 3;

        now

          let n be Nat;

          (a . n) <= (b . n) by A1;

          then (a . n) <= r by A6, XXREAL_0: 2;

          then ((a . n) + 0 ) < (r + 1) by XREAL_1: 8;

          hence (a . n) < (r + 1);

        end;

        hence thesis by SEQ_2:def 3;

      end;

      hence a is convergent by A3;

      thus thesis by A1, A2, A3, A5, SEQ_2: 18;

    end;

    theorem :: HOLDER_1:9

    

     Th9: for a,b,c be Real_Sequence st (for n be Nat holds (a . n) <= ((b . n) + (c . n))) & b is convergent & c is convergent & a is non-decreasing holds a is convergent & ( lim a) <= (( lim b) + ( lim c))

    proof

      let a,b,c be Real_Sequence such that

       A1: for n be Nat holds (a . n) <= ((b . n) + (c . n)) and

       A2: b is convergent & c is convergent and

       A3: a is non-decreasing;

       A4:

      now

        let n be Nat;

        (a . n) <= ((b . n) + (c . n)) by A1;

        hence (a . n) <= ((b + c) . n) by SEQ_1: 7;

      end;

      

       A5: (b + c) is convergent by A2;

      hence a is convergent by A3, A4, Th8;

      ( lim (b + c)) = (( lim b) + ( lim c)) by A2, SEQ_2: 6;

      hence thesis by A3, A5, A4, Th8;

    end;

    theorem :: HOLDER_1:10

    

     Th10: for p be Real st 0 < p holds for a,ap be Real_Sequence st a is convergent & (for n be Nat holds 0 <= (a . n)) & (for n be Nat holds (ap . n) = ((a . n) to_power p)) holds ap is convergent & ( lim ap) = (( lim a) to_power p)

    proof

      let p be Real such that

       A1: 0 < p;

      let a,ap be Real_Sequence such that

       A2: a is convergent and

       A3: for n be Nat holds 0 <= (a . n) and

       A4: for n be Nat holds (ap . n) = ((a . n) to_power p);

      now

        per cases ;

          case

           A5: ( lim a) = 0 ;

          now

            per cases ;

              case ex n be Nat st for m be Nat st n <= m holds (a . m) = 0 ;

              then

              consider N be Nat such that

               A6: for m be Nat st N <= m holds (a . m) = 0 ;

              

               A7: for n be Nat holds ((a ^\ N) . n) = 0

              proof

                let n be Nat;

                (a . (n + N)) = 0 by A6, NAT_1: 12;

                hence thesis by NAT_1:def 3;

              end;

               A8:

              now

                let e be Real such that

                 A9: e > 0 ;

                reconsider n = 0 as Nat;

                take n;

                let m be Nat such that n <= m;

                

                 A10: (( lim a) to_power p) = 0 by A1, A5, POWER:def 2;

                ((ap ^\ N) . m) = (ap . (m + N)) by NAT_1:def 3

                .= ((a . (m + N)) to_power p) by A4

                .= (((a ^\ N) . m) to_power p) by NAT_1:def 3

                .= ( 0 to_power p) by A7

                .= 0 by A1, POWER:def 2;

                hence |.(((ap ^\ N) . m) - (( lim a) to_power p)).| < e by A9, A10, ABSVALUE: 2;

              end;

              then

               A11: (ap ^\ N) is convergent by SEQ_2:def 6;

              then (( lim a) to_power p) = ( lim (ap ^\ N)) by A8, SEQ_2:def 7;

              hence thesis by A11, SEQ_4: 20, SEQ_4: 21;

            end;

              case

               A12: for n be Nat holds ex m be Nat st n <= m & (a . m) <> 0 ;

              defpred P[ set] means (a . $1) <> 0 ;

              ex m1 be Nat st 0 <= m1 & (a . m1) <> 0 by A12;

              then

               A13: ex m be Nat st P[m];

              consider M be Nat such that

               A14: P[M] & for n be Nat st P[n] holds M <= n from NAT_1:sch 5( A13);

              defpred P[ set, set, set] means for n,m be Nat st $2 = n & $3 = m holds n < m & (a . m) <> 0 & for k be Nat st n < k & (a . k) <> 0 holds m <= k;

              

               A15: (( lim a) to_power p) = 0 by A1, A5, POWER:def 2;

              reconsider M as Nat;

               A16:

              now

                let n be Nat;

                consider m be Nat such that

                 A17: (n + 1) <= m & (a . m) <> 0 by A12;

                take m;

                thus n < m & (a . m) <> 0 by A17, NAT_1: 13;

              end;

              

               A18: for n be Nat, x be Element of NAT holds ex y be Element of NAT st P[n, x, y]

              proof

                let n be Nat, x be Element of NAT ;

                defpred P[ Nat] means x < $1 & (a . $1) <> 0 ;

                ex m be Nat st P[m] by A16;

                then

                 A19: ex m be Nat st P[m];

                consider l be Nat such that

                 A20: P[l] & for k be Nat st P[k] holds l <= k from NAT_1:sch 5( A19);

                take l;

                l in NAT by ORDINAL1:def 12;

                hence thesis by A20;

              end;

              reconsider zz = 0 as Element of NAT ;

              consider F be sequence of NAT such that

               A21: (F . 0 ) = ( In (M, NAT )) & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A18);

              ( rng F) c= NAT by RELAT_1:def 19;

              then

               A22: ( rng F) c= REAL by NUMBERS: 19;

              ( dom F) = NAT by FUNCT_2:def 1;

              then

              reconsider F as Real_Sequence by A22, RELSET_1: 4;

              for n be Nat holds (F . n) < (F . (n + 1)) by A21;

              then

              reconsider F as increasing sequence of NAT by SEQM_3:def 6;

              

               A23: for n be Nat st (a . n) <> 0 holds ex m be Nat st (F . m) = n

              proof

                defpred P[ set] means (a . $1) <> 0 & for m be Nat holds (F . m) <> $1;

                assume ex n be Nat st P[n];

                then

                 A24: ex n be Nat st P[n];

                consider M1 be Nat such that

                 A25: P[M1] & for n be Nat st P[n] holds M1 <= n from NAT_1:sch 5( A24);

                defpred P[ Nat] means $1 < M1 & (a . $1) <> 0 & ex m be Nat st (F . m) = $1;

                

                 A26: ex n be Nat st P[n]

                proof

                  take M;

                  M <= M1 & M <> M1 by A14, A21, A25;

                  hence M < M1 by XXREAL_0: 1;

                  thus (a . M) <> 0 by A14;

                  take 0 ;

                  thus thesis by A21;

                end;

                

                 A27: for n be Nat st P[n] holds n <= M1;

                consider MX be Nat such that

                 A28: P[MX] & for n be Nat st P[n] holds n <= MX from NAT_1:sch 6( A27, A26);

                

                 A29: for k be Nat st MX < k & k < M1 holds (a . k) = 0

                proof

                  given k be Nat such that

                   A30: MX < k and

                   A31: k < M1 & (a . k) <> 0 ;

                  now

                    per cases ;

                      case ex m be Nat st (F . m) = k;

                      hence contradiction by A28, A30, A31;

                    end;

                      case for m be Nat holds (F . m) <> k;

                      hence contradiction by A25, A31;

                    end;

                  end;

                  hence contradiction;

                end;

                consider m be Nat such that

                 A32: (F . m) = MX by A28;

                

                 A33: MX < (F . (m + 1)) & (a . (F . (m + 1))) <> 0 by A21, A32;

                

                 A34: (F . (m + 1)) <= M1 by A21, A25, A28, A32;

                now

                  assume (F . (m + 1)) <> M1;

                  then (F . (m + 1)) < M1 by A34, XXREAL_0: 1;

                  hence contradiction by A29, A33;

                end;

                hence contradiction by A25;

              end;

              

               A35: (a * F) is convergent & ( lim (a * F)) = 0 by A2, A5, SEQ_4: 16, SEQ_4: 17;

               A36:

              now

                let e be Real;

                assume

                 A37: 0 < e;

                then 0 < (e to_power (1 / p)) by POWER: 34;

                then

                consider n be Nat such that

                 A38: for m be Nat st n <= m holds |.(((a * F) . m) - 0 ).| < (e to_power (1 / p)) by A35, SEQ_2:def 7;

                reconsider k = (F . n) as Nat;

                take k;

                let m be Nat such that

                 A39: k <= m;

                now

                  per cases ;

                    case (a . m) = 0 ;

                    

                    then (ap . m) = ( 0 to_power p) by A4

                    .= 0 by A1, POWER:def 2;

                    hence |.((ap . m) - (( lim a) to_power p)).| < e by A15, A37, ABSVALUE: 2;

                  end;

                    case

                     A40: (a . m) <> 0 ;

                    then

                    consider l be Nat such that

                     A41: m = (F . l) by A23;

                    

                     A42: l in NAT by ORDINAL1:def 12;

                    n <= l by A39, A41, SEQM_3: 1;

                    then |.(((a * F) . l) - 0 ).| < (e to_power (1 / p)) by A38;

                    then

                     A43: |.(a . (F . l)).| < (e to_power (1 / p)) by FUNCT_2: 15, A42;

                    

                     A44: ((a . m) to_power p) = (ap . m) by A4;

                    

                     A45: (a . m) > 0 by A3, A40;

                    then

                     A46: 0 < (ap . m) by A44, POWER: 34;

                     |.(a . m).| > 0 by A40, COMPLEX1: 47;

                    then ( |.(a . m).| to_power p) < ((e to_power (1 / p)) to_power p) by A1, A41, A43, POWER: 37;

                    then ( |.(a . m).| to_power p) < (e to_power ((1 / p) * p)) by A37, POWER: 33;

                    then ( |.(a . m).| to_power p) < (e to_power 1) by A1, XCMPLX_1: 106;

                    then ( |.(a . m).| to_power p) < e by POWER: 25;

                    then (ap . m) < e by A45, A44, ABSVALUE:def 1;

                    hence |.((ap . m) - (( lim a) to_power p)).| < e by A15, A46, ABSVALUE:def 1;

                  end;

                end;

                hence |.((ap . m) - (( lim a) to_power p)).| < e;

              end;

              hence ap is convergent by SEQ_2:def 6;

              hence ( lim ap) = (( lim a) to_power p) by A36, SEQ_2:def 7;

            end;

          end;

          hence thesis;

        end;

          case

           A47: ( lim a) <> 0 ;

          

           A48: 0 <= ( lim a) by A2, A3, SEQ_2: 17;

          ex k be Nat st ( rng (a ^\ k)) c= ( dom ( #R p))

          proof

            set e0 = ( lim a);

            

             A49: (e0 / 2) > 0 by A47, A48, XREAL_1: 215;

            then

            consider k be Nat such that

             A50: for m be Nat st k <= m holds |.((a . m) - e0).| < (e0 / 2) by A2, SEQ_2:def 7;

            take k;

             A51:

            now

              let m be Nat;

               |.((a . (k + m)) - e0).| < (e0 / 2) by A50, NAT_1: 12;

              then ( - (e0 / 2)) <= ((a . (k + m)) - e0) by ABSVALUE: 5;

              then (( - (e0 / 2)) + e0) <= (((a . (k + m)) - e0) + e0) by XREAL_1: 7;

              hence 0 < ((a ^\ k) . m) by A49, NAT_1:def 3;

            end;

            let x be object;

            assume x in ( rng (a ^\ k));

            then

            consider n be Element of NAT such that

             A52: x = ((a ^\ k) . n) by FUNCT_2: 113;

             0 < ((a ^\ k) . n) by A51;

            then ((a ^\ k) . n) in { g where g be Real : 0 < g };

            then ((a ^\ k) . n) in ( right_open_halfline 0 ) by XXREAL_1: 230;

            hence x in ( dom ( #R p)) by A52, TAYLOR_1:def 4;

          end;

          then

          consider k be Nat such that

           A53: ( rng (a ^\ k)) c= ( dom ( #R p));

          now

            let x be object;

            assume x in NAT ;

            then

            reconsider n = x as Element of NAT ;

            ((a ^\ k) . n) in ( rng (a ^\ k)) by VALUED_0: 28;

            then ((a ^\ k) . n) in ( dom ( #R p)) by A53;

            then

             A54: ((a ^\ k) . n) in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

            then (a . (k + n)) in ( right_open_halfline 0 ) by NAT_1:def 3;

            then (a . (k + n)) in { g where g be Real : 0 < g } by XXREAL_1: 230;

            then

             A55: ex g be Real st (a . (k + n)) = g & g > 0 ;

            

            thus ((( #R p) /* (a ^\ k)) . x) = (( #R p) . ((a ^\ k) . n)) by A53, FUNCT_2: 108

            .= (((a ^\ k) . n) #R p) by A54, TAYLOR_1:def 4

            .= ((a . (k + n)) #R p) by NAT_1:def 3

            .= ((a . (k + n)) to_power p) by A55, POWER:def 2

            .= (ap . (k + n)) by A4

            .= ((ap ^\ k) . x) by NAT_1:def 3;

          end;

          then

           A56: (( #R p) /* (a ^\ k)) = (ap ^\ k) by FUNCT_2: 12;

          

           A57: ( lim (a ^\ k)) = ( lim a) by A2, SEQ_4: 20;

          ( lim a) > 0 by A2, A3, A47, SEQ_2: 17;

          then ( #R p) is_continuous_in ( lim (a ^\ k)) by A57, FDIFF_1: 24, TAYLOR_1: 21;

          then

           A58: (( #R p) /* (a ^\ k)) is convergent & (( #R p) . ( lim (a ^\ k))) = ( lim (( #R p) /* (a ^\ k))) by A2, A53, FCONT_1:def 1;

          ( lim a) in { g where g be Real : 0 < g } by A47, A48;

          then ( lim a) in ( right_open_halfline 0 ) by XXREAL_1: 230;

          

          then (( #R p) . ( lim (a ^\ k))) = (( lim a) #R p) by A57, TAYLOR_1:def 4

          .= (( lim a) to_power p) by A47, A48, POWER:def 2;

          hence thesis by A58, A56, SEQ_4: 21, SEQ_4: 22;

        end;

      end;

      hence thesis;

    end;

    theorem :: HOLDER_1:11

    for p be Real st 0 < p holds for a,ap be Real_Sequence st a is summable & (for n be Nat holds 0 <= (a . n)) & (for n be Nat holds (ap . n) = ((( Partial_Sums a) . n) to_power p)) holds ap is convergent & ( lim ap) = (( Sum a) to_power p) & ap is non-decreasing & for n be Nat holds (ap . n) <= (( Sum a) to_power p)

    proof

      let p be Real such that

       A1: 0 < p;

      let a,ap be Real_Sequence such that

       A2: a is summable and

       A3: for n be Nat holds 0 <= (a . n) and

       A4: for n be Nat holds (ap . n) = ((( Partial_Sums a) . n) to_power p);

      

       A5: ( Partial_Sums a) is convergent & for n be Nat holds 0 <= (( Partial_Sums a) . n) by A2, A3, Lm2, SERIES_1:def 2;

      then ( lim ap) = (( lim ( Partial_Sums a)) to_power p) by A1, A4, Th10;

      hence

       A6: ap is convergent & ( lim ap) = (( Sum a) to_power p) by A1, A4, A5, Th10, SERIES_1:def 3;

      

       A7: ( Partial_Sums a) is non-decreasing by A3, SERIES_1: 16;

      now

        let n,m be Nat;

        assume n <= m;

        then

         A8: (( Partial_Sums a) . n) <= (( Partial_Sums a) . m) by A7, SEQM_3: 6;

        

         A9: (ap . n) = ((( Partial_Sums a) . n) to_power p) & (ap . m) = ((( Partial_Sums a) . m) to_power p) by A4;

         0 <= (( Partial_Sums a) . n) by A3, Lm2;

        hence (ap . n) <= (ap . m) by A1, A9, A8, Th3;

      end;

      hence

       A10: ap is non-decreasing by SEQM_3: 6;

      thus thesis by A6, A10, SEQ_4: 37;

    end;

    theorem :: HOLDER_1:12

    for p,q be Real st 1 < p & ((1 / p) + (1 / q)) = 1 holds for a,b,ap,bq,ab be Real_Sequence st (for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bq . n) = ( |.(b . n).| to_power q) & (ab . n) = |.((a . n) * (b . n)).|) & ap is summable & bq is summable holds ab is summable & ( Sum ab) <= ((( Sum ap) to_power (1 / p)) * (( Sum bq) to_power (1 / q)))

    proof

      let p,q be Real such that

       A1: 1 < p and

       A2: ((1 / p) + (1 / q)) = 1;

      let a,b,ap,bq,ab be Real_Sequence such that

       A3: for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bq . n) = ( |.(b . n).| to_power q) & (ab . n) = |.((a . n) * (b . n)).| and

       A4: ap is summable and

       A5: bq is summable;

      

       A6: ( Partial_Sums ap) is convergent by A4, SERIES_1:def 2;

      reconsider pp = (1 / p) as Real;

      (1 / p) < 1 by A1, XREAL_1: 189;

      then

       A7: (1 - 1) < (1 - pp) by XREAL_1: 15;

      then

       A8: 0 < q by A2;

      for n be Nat holds 0 <= (bq . n)

      proof

        let n be Nat;

        

         A9: (bq . n) = ( |.(b . n).| to_power q) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(b . n).| = 0 ;

            hence thesis by A8, A9, POWER:def 2;

          end;

            case |.(b . n).| > 0 ;

            hence thesis by A9, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      then

       A10: for n be Nat holds 0 <= (( Partial_Sums bq) . n) by Lm2;

      for n be Nat holds 0 <= (ab . n)

      proof

        let n be Nat;

        (ab . n) = |.((a . n) * (b . n)).| by A3;

        hence thesis by COMPLEX1: 46;

      end;

      then

       A11: ( Partial_Sums ab) is non-decreasing by SERIES_1: 16;

      deffunc G( Nat) = ((( Partial_Sums bq) . $1) to_power (1 / q));

      consider y be Real_Sequence such that

       A12: for n be Nat holds (y . n) = G(n) from SEQ_1:sch 1;

      for n be Nat holds 0 <= (ap . n)

      proof

        let n be Nat;

        

         A13: (ap . n) = ( |.(a . n).| to_power p) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(a . n).| = 0 ;

            hence thesis by A1, A13, POWER:def 2;

          end;

            case |.(a . n).| > 0 ;

            hence thesis by A13, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      then

       A14: for n be Nat holds 0 <= (( Partial_Sums ap) . n) by Lm2;

      deffunc F( Nat) = ((( Partial_Sums ap) . $1) to_power (1 / p));

      consider x be Real_Sequence such that

       A15: for n be Nat holds (x . n) = F(n) from SEQ_1:sch 1;

      

       A16: for n be Nat holds (( Partial_Sums ab) . n) <= ((x (#) y) . n)

      proof

        let n be Nat;

        

         A17: (y . n) = ((( Partial_Sums bq) . n) to_power (1 / q)) by A12;

        (( Partial_Sums ab) . n) <= (((( Partial_Sums ap) . n) to_power (1 / p)) * ((( Partial_Sums bq) . n) to_power (1 / q))) & (x . n) = ((( Partial_Sums ap) . n) to_power (1 / p)) by A1, A2, A3, A15, Th6;

        hence thesis by A17, SEQ_1: 8;

      end;

      

       A18: (1 / p) > 0 by A1, XREAL_1: 139;

      then

       A19: x is convergent by A15, A6, A14, Th10;

      

       A20: ( Partial_Sums bq) is convergent by A5, SERIES_1:def 2;

      then

       A21: y is convergent by A2, A7, A12, A10, Th10;

      then (x (#) y) is convergent by A19;

      then

       A22: ( Partial_Sums ab) is convergent & ( lim ( Partial_Sums ab)) <= ( lim (x (#) y)) by A16, A11, Th8;

      ( Sum ap) = ( lim ( Partial_Sums ap)) by SERIES_1:def 3;

      then

       A23: ( lim x) = (( Sum ap) to_power (1 / p)) by A18, A15, A6, A14, Th10;

      ( Sum bq) = ( lim ( Partial_Sums bq)) by SERIES_1:def 3;

      then ( lim y) = (( Sum bq) to_power (1 / q)) by A2, A7, A12, A20, A10, Th10;

      then ( lim (x (#) y)) = ((( Sum ap) to_power (1 / p)) * (( Sum bq) to_power (1 / q))) by A19, A23, A21, SEQ_2: 15;

      hence thesis by A22, SERIES_1:def 2, SERIES_1:def 3;

    end;

    theorem :: HOLDER_1:13

    for p be Real st 1 < p holds for a,b,ap,bp,ab be Real_Sequence st (for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bp . n) = ( |.(b . n).| to_power p) & (ab . n) = ( |.((a . n) + (b . n)).| to_power p)) & ap is summable & bp is summable holds ab is summable & (( Sum ab) to_power (1 / p)) <= ((( Sum ap) to_power (1 / p)) + (( Sum bp) to_power (1 / p)))

    proof

      let p be Real such that

       A1: 1 < p;

      

       A2: (1 / p) > 0 by A1, XREAL_1: 139;

      let a,b,ap,bp,ab be Real_Sequence such that

       A3: for n be Nat holds (ap . n) = ( |.(a . n).| to_power p) & (bp . n) = ( |.(b . n).| to_power p) & (ab . n) = ( |.((a . n) + (b . n)).| to_power p) and

       A4: ap is summable and

       A5: bp is summable;

      deffunc H( Nat) = ((( Partial_Sums ab) . $1) to_power (1 / p));

      consider z be Real_Sequence such that

       A6: for n be Nat holds (z . n) = H(n) from SEQ_1:sch 1;

      

       A7: for n be Nat holds 0 <= (ab . n)

      proof

        let n be Nat;

        

         A8: (ab . n) = ( |.((a . n) + (b . n)).| to_power p) by A3;

        per cases by COMPLEX1: 46;

          suppose |.((a . n) + (b . n)).| = 0 ;

          hence thesis by A1, A8, POWER:def 2;

        end;

          suppose |.((a . n) + (b . n)).| > 0 ;

          hence thesis by A8, POWER: 34;

        end;

      end;

      

       A9: for n be Nat holds 0 <= (z . n)

      proof

        let n be Nat;

        

         A10: (z . n) = ((( Partial_Sums ab) . n) to_power (1 / p)) by A6;

        per cases by A7, Lm2;

          suppose (( Partial_Sums ab) . n) = 0 ;

          hence thesis by A2, A10, POWER:def 2;

        end;

          suppose (( Partial_Sums ab) . n) > 0 ;

          hence thesis by A10, POWER: 34;

        end;

      end;

      

       A11: ( Partial_Sums ab) is non-decreasing by A7, SERIES_1: 16;

       A12:

      now

        let n,m be Nat;

        assume n <= m;

        then

         A13: (( Partial_Sums ab) . n) <= (( Partial_Sums ab) . m) by A11, SEQM_3: 6;

        

         A14: 0 <= ((( Partial_Sums ab) . m) to_power (1 / p))

        proof

          per cases by A7, Lm2;

            suppose (( Partial_Sums ab) . m) = 0 ;

            hence thesis by A2, POWER:def 2;

          end;

            suppose (( Partial_Sums ab) . m) > 0 ;

            hence thesis by POWER: 34;

          end;

        end;

        now

          per cases ;

            case (( Partial_Sums ab) . n) = (( Partial_Sums ab) . m);

            hence ((( Partial_Sums ab) . n) to_power (1 / p)) <= ((( Partial_Sums ab) . m) to_power (1 / p));

          end;

            case (( Partial_Sums ab) . n) <> (( Partial_Sums ab) . m);

            then

             A15: (( Partial_Sums ab) . n) < (( Partial_Sums ab) . m) by A13, XXREAL_0: 1;

            now

              per cases ;

                case (( Partial_Sums ab) . n) = 0 ;

                hence ((( Partial_Sums ab) . n) to_power (1 / p)) <= ((( Partial_Sums ab) . m) to_power (1 / p)) by A2, A14, POWER:def 2;

              end;

                case

                 A16: (( Partial_Sums ab) . n) <> 0 ;

                 0 <= (( Partial_Sums ab) . n) by A7, Lm2;

                hence ((( Partial_Sums ab) . n) to_power (1 / p)) <= ((( Partial_Sums ab) . m) to_power (1 / p)) by A2, A15, A16, POWER: 37;

              end;

            end;

            hence ((( Partial_Sums ab) . n) to_power (1 / p)) <= ((( Partial_Sums ab) . m) to_power (1 / p));

          end;

        end;

        hence ((( Partial_Sums ab) . n) to_power (1 / p)) <= ((( Partial_Sums ab) . m) to_power (1 / p));

      end;

      now

        let n,m be Nat;

        assume

         A17: n <= m;

        (z . n) = ((( Partial_Sums ab) . n) to_power (1 / p)) & (z . m) = ((( Partial_Sums ab) . m) to_power (1 / p)) by A6;

        hence (z . n) <= (z . m) by A12, A17;

      end;

      then

       A18: z is non-decreasing by SEQM_3: 6;

      for n be Nat holds 0 <= (ap . n)

      proof

        let n be Nat;

        

         A19: (ap . n) = ( |.(a . n).| to_power p) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(a . n).| = 0 ;

            hence thesis by A1, A19, POWER:def 2;

          end;

            case |.(a . n).| > 0 ;

            hence thesis by A19, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      then

       A20: for n be Nat holds 0 <= (( Partial_Sums ap) . n) by Lm2;

      deffunc F( Nat) = ((( Partial_Sums ap) . $1) to_power (1 / p));

      consider x be Real_Sequence such that

       A21: for n be Nat holds (x . n) = F(n) from SEQ_1:sch 1;

      for n be Nat holds 0 <= (bp . n)

      proof

        let n be Nat;

        

         A22: (bp . n) = ( |.(b . n).| to_power p) by A3;

        now

          per cases by COMPLEX1: 46;

            case |.(b . n).| = 0 ;

            hence thesis by A1, A22, POWER:def 2;

          end;

            case |.(b . n).| > 0 ;

            hence thesis by A22, POWER: 34;

          end;

        end;

        hence thesis;

      end;

      then

       A23: for n be Nat holds 0 <= (( Partial_Sums bp) . n) by Lm2;

      deffunc G( Nat) = ((( Partial_Sums bp) . $1) to_power (1 / p));

      consider y be Real_Sequence such that

       A24: for n be Nat holds (y . n) = G(n) from SEQ_1:sch 1;

      

       A25: ( Partial_Sums bp) is convergent by A5, SERIES_1:def 2;

      then

       A26: y is convergent by A2, A24, A23, Th10;

      

       A27: ( Partial_Sums ap) is convergent by A4, SERIES_1:def 2;

      then

       A28: x is convergent by A2, A21, A20, Th10;

      

       A29: for n be Nat holds (z . n) <= ((x . n) + (y . n))

      proof

        let n be Nat;

        

         A30: (y . n) = ((( Partial_Sums bp) . n) to_power (1 / p)) by A24;

        ((( Partial_Sums ab) . n) to_power (1 / p)) <= (((( Partial_Sums ap) . n) to_power (1 / p)) + ((( Partial_Sums bp) . n) to_power (1 / p))) & (x . n) = ((( Partial_Sums ap) . n) to_power (1 / p)) by A1, A3, A21, Th7;

        hence thesis by A6, A30;

      end;

      then

       A31: z is convergent by A28, A26, A18, Th9;

      

       A32: for n be Nat holds ((z . n) to_power p) = (( Partial_Sums ab) . n)

      proof

        let n be Nat;

        

         A33: (z . n) = ((( Partial_Sums ab) . n) to_power (1 / p)) by A6;

        now

          per cases ;

            case

             A34: (( Partial_Sums ab) . n) = 0 ;

            then (z . n) = 0 by A2, A33, POWER:def 2;

            hence thesis by A1, A34, POWER:def 2;

          end;

            case

             A35: (( Partial_Sums ab) . n) <> 0 ;

             0 <= (( Partial_Sums ab) . n) by A7, Lm2;

            

            hence ((z . n) to_power p) = ((( Partial_Sums ab) . n) to_power ((1 / p) * p)) by A33, A35, POWER: 33

            .= ((( Partial_Sums ab) . n) to_power 1) by A1, XCMPLX_1: 106

            .= (( Partial_Sums ab) . n) by POWER: 25;

          end;

        end;

        hence thesis;

      end;

      then ( lim ( Partial_Sums ab)) = (( lim z) to_power p) by A1, A9, A31, Th10;

      then

       A36: ( Sum ab) = (( lim z) to_power p) by SERIES_1:def 3;

      

       A37: (( Sum ab) to_power (1 / p)) = ( lim z)

      proof

        per cases ;

          suppose

           A38: ( lim z) = 0 ;

          

          hence (( Sum ab) to_power (1 / p)) = ( 0 to_power (1 / p)) by A1, A36, POWER:def 2

          .= ( lim z) by A2, A38, POWER:def 2;

        end;

          suppose ( lim z) <> 0 ;

          then 0 < ( lim z) by A9, A31, SEQ_2: 17;

          

          hence (( Sum ab) to_power (1 / p)) = (( lim z) to_power ((1 / p) * p)) by A36, POWER: 33

          .= (( lim z) to_power 1) by A1, XCMPLX_1: 106

          .= ( lim z) by POWER: 25;

        end;

      end;

      ( Sum bp) = ( lim ( Partial_Sums bp)) by SERIES_1:def 3;

      then

       A39: ( lim y) = (( Sum bp) to_power (1 / p)) by A2, A24, A25, A23, Th10;

      ( Sum ap) = ( lim ( Partial_Sums ap)) by SERIES_1:def 3;

      then

       A40: ( lim x) = (( Sum ap) to_power (1 / p)) by A2, A21, A27, A20, Th10;

      ( Partial_Sums ab) is convergent by A1, A9, A31, A32, Th10;

      hence thesis by A28, A40, A26, A39, A29, A18, A37, Th9, SERIES_1:def 2;

    end;