derivative_comp_from_args

forall (Scalar : Sort u), forall (zero : Scalar), forall (one : Scalar), forall (add : forall (a : Scalar), forall (b : Scalar), Scalar), forall (neg : forall (a : Scalar), Scalar), forall (sub : forall (a : Scalar), forall (b : Scalar), Scalar), forall (mul : forall (a : Scalar), forall (b : Scalar), Scalar), forall (le_rel : forall (a : Scalar), forall (b : Scalar), Prop), forall (X : Sort v), forall (xzero : X), forall (xadd : forall (x : X), forall (y : X), X), forall (xneg : forall (x : X), X), forall (xsmul : forall (a : Scalar), forall (x : X), X), forall (xnorm : forall (x : X), Scalar), forall (Y : Sort w), forall (yzero : Y), forall (yadd : forall (x : Y), forall (y : Y), Y), forall (yneg : forall (y : Y), Y), forall (ysmul : forall (a : Scalar), forall (y : Y), Y), forall (ynorm : forall (y : Y), Scalar), forall (Z : Sort z), forall (zzero : Z), forall (zadd : forall (x : Z), forall (y : Z), Z), forall (zneg : forall (z : Z), Z), forall (zsmul : forall (a : Scalar), forall (z : Z), Z), forall (znorm : forall (z : Z), Scalar), forall (f : forall (x : X), Y), forall (g : forall (y : Y), Z), forall (args : @DerivativeCompRuleArgs.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g), forall (point : X), forall (df : forall (h : X), Y), forall (dg : forall (h : Y), Z), forall (f_bound : Scalar), forall (f_remainder : forall (r : Y), Prop), forall (g_bound : Scalar), forall (g_remainder : forall (r : Z), Prop), forall (comp_bound : Scalar), forall (comp_remainder : forall (r : Z), Prop), forall (f_at : @FrechetDerivativeAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm f point df f_bound f_remainder), forall (g_at : @FrechetDerivativeAt.{u,w,z} Scalar zero one add neg sub mul le_rel Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm g (f point) dg g_bound g_remainder), @FrechetDerivativeAt.{u,v,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Z zzero zadd zneg zsmul znorm (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm f g) point (@LinearComp.{u,v,w,z} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm Z zzero zadd zneg zsmul znorm df dg) comp_bound comp_remainder

fun Scalar => fun zero => fun one => fun add => fun neg => fun sub => fun mul => fun le_rel => fun X => fun xzero => fun xadd => fun xneg => fun xsmul => fun xnorm => fun Y => fun yzero => fun yadd => fun yneg => fun ysmul => fun ynorm => fun Z => fun zzero => fun zadd => fun zneg => fun zsmul => fun znorm => fun f => fun g => fun args => fun point => fun df => fun dg => fun f_bound => fun f_remainder => fun g_bound => fun g_remainder => fun comp_bound => fun comp_remainder => fun f_at => fun g_at => args point df dg f_bound f_remainder g_bound g_remainder comp_bound comp_remainder f_at g_at