今回は # g`!x:num->real. x tends_num_real &0 ==> (\n. sum(1..n)x / &n) tends_num_real &0`;; val it : goalstack = 1 subgoal (1 total)`!x. x tends_num_real &0 ==> (\n. sum (1..n) x / &n) tends_num_real &0` です．数学的には分割して評価する標…

sos.mlには，次の定理が含まれています． # search[name"SOS"];; val it : (string * thm) list = [("INT_SOS_EQ_0", |- !x y. x pow 2 + y pow 2 = &0 x = &0 /\ y = &0); ("REAL_SOS_EQ_0", |- !x y. x pow 2 + y pow 2 = &0 x = &0 /\ y = &0)] 今回はこ…