proposition: Lemma continuous_unary : forall unop a b x, no_floor_op unop = true -> (notXnan b -> b = Xreal (a x) /\ continuous a x) -> notXnan (unary ext_operations unop b) -> unary ext_operations unop b = Xreal (unary real_operations unop (a x)) /\ continuous (fun x0 : R => unary real_operations unop (a x0)) x.
proof: Proof. move => unop a b x NF Hb HbnotXnan. case Hbnan: b Hb => [|b1] // Hb. rewrite Hbnan /= in HbnotXnan. by case unop in HbnotXnan. case: Hb => // Hb Hcontax. move: HbnotXnan. rewrite Hbnan Hb => {Hbnan Hb b1} HnotXnan. split. (case: unop NF HnotXnan; try discriminate) => //= [_|_|_|]. - rewrite /Xinv'. by case is_zero. - rewrite /Xtan'. by case is_zero. - rewrite /Xln'. by case is_positive. - case => [||p] //. rewrite /Xpower_int'. by case is_zero. (case: unop NF HnotXnan; try discriminate) => //= [_|_|_|_|_|_|_|_|_|_|_|]. - move => _. by apply: continuous_opp. - move => _. by apply: continuous_Rabs_comp. - move => HnotXnan. apply: continuous_Rinv_comp => // Ha. move: HnotXnan. by rewrite /Xinv' Ha is_zero_0. - move => _. by apply: continuous_mult. - move => HnotXnan. exact: continuous_sqrt_comp. - move => _. by apply: continuous_cos_comp. - move => _. by apply: continuous_sin_comp. - move => HnotXnan. apply: continuous_comp => //. apply: continuous_tan => Ha. move: HnotXnan. by rewrite /Xtan' Ha is_zero_0. - move => _. by apply: continuous_atan_comp. - move => _. by apply: continuous_exp_comp. - move => HnotXnan. apply: continuous_comp => //. apply: continuous_ln. rewrite /Xln' in HnotXnan. by case: is_positive_spec HnotXnan. - move => n. rewrite /powerRZ. case: n => [|n|n] _ HnotXnan. + exact: continuous_const. + apply: (continuous_comp a (fun x => pow x _)) => //. apply: ex_derive_continuous. apply: ex_derive_pow. exact: ex_derive_id. + rewrite /Xpower_int' in HnotXnan. case: is_zero_spec HnotXnan => // Ha _. apply: continuous_comp. apply: (continuous_comp a (fun x => pow x _)) => //. apply: ex_derive_continuous. apply: ex_derive_pow. exact: ex_derive_id. apply: continuous_Rinv. exact: pow_nonzero. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog