implicit_function_derivative_evidence_formula

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 (XY : Sort p), forall (xyzero : XY), forall (xyadd : forall (x : XY), forall (y : XY), XY), forall (xyneg : forall (x : XY), XY), forall (xysmul : forall (a : Scalar), forall (x : XY), XY), forall (xynorm : forall (x : XY), Scalar), forall (pairXY : forall (x : X), forall (y : Y), XY), forall (fstXY : forall (point : XY), X), forall (sndXY : forall (point : XY), Y), forall (XZ : Sort q), forall (xzzero : XZ), forall (xzadd : forall (x : XZ), forall (y : XZ), XZ), forall (xzneg : forall (x : XZ), XZ), forall (xzsmul : forall (a : Scalar), forall (x : XZ), XZ), forall (xznorm : forall (x : XZ), Scalar), forall (pairXZ : forall (x : X), forall (z : Z), XZ), forall (fstXZ : forall (point : XZ), X), forall (sndXZ : forall (point : XZ), Z), forall (F : forall (point : XY), Z), forall (base_x : X), forall (base_y : Y), forall (x_domain : forall (x : X), Prop), forall (y_domain : forall (y : Y), Prop), forall (xy_domain : forall (point : XY), Prop), forall (xz_domain : forall (target : XZ), Prop), forall (phi_inv : forall (target : XZ), XY), forall (dPhi : forall (h : XY), XZ), forall (dPhi_inv : forall (target : XZ), XY), forall (op_norm : Scalar), forall (inv_op_norm : Scalar), forall (inverse_bound : Scalar), forall (inverse_remainder : forall (r : XY), Prop), forall (dFx : forall (x : X), forall (h : X), Z), forall (dFy : forall (x : X), forall (h : Y), Z), forall (dFy_inv : forall (x : X), forall (z : Z), Y), forall (dPhi_inv_at : forall (x : X), forall (target : XZ), XY), forall (target_bound : Scalar), forall (target_remainder : forall (r : XZ), Prop), forall (partial_x_bound : Scalar), forall (partial_x_remainder : forall (r : Z), Prop), forall (partial_y_bound : Scalar), forall (partial_y_remainder : forall (r : Z), Prop), forall (dy_op_norm : Scalar), forall (dy_inv_op_norm : Scalar), forall (phi_inverse_bound : Scalar), forall (phi_inverse_remainder : forall (r : XY), Prop), forall (snd_bound : Scalar), forall (snd_remainder : forall (r : Y), Prop), forall (chain_bound : Scalar), forall (chain_remainder : forall (r : Y), Prop), forall (evidence : @ImplicitFunctionDerivativeEvidence.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dFx dFy dFy_inv dPhi_inv_at target_bound target_remainder partial_x_bound partial_x_remainder partial_y_bound partial_y_remainder dy_op_norm dy_inv_op_norm phi_inverse_bound phi_inverse_remainder snd_bound snd_remainder chain_bound chain_remainder), forall (x : X), forall (hx : x_domain x), forall (h : X), @Eq.{w} Y (@ImplicitFunctionDerivativeChainMap.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dPhi_inv_at x h) (@ImplicitFunctionDerivativeFormulaMap.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dFx dFy_inv x h)

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 XY => fun xyzero => fun xyadd => fun xyneg => fun xysmul => fun xynorm => fun pairXY => fun fstXY => fun sndXY => fun XZ => fun xzzero => fun xzadd => fun xzneg => fun xzsmul => fun xznorm => fun pairXZ => fun fstXZ => fun sndXZ => fun F => fun base_x => fun base_y => fun x_domain => fun y_domain => fun xy_domain => fun xz_domain => fun phi_inv => fun dPhi => fun dPhi_inv => fun op_norm => fun inv_op_norm => fun inverse_bound => fun inverse_remainder => fun dFx => fun dFy => fun dFy_inv => fun dPhi_inv_at => fun target_bound => fun target_remainder => fun partial_x_bound => fun partial_x_remainder => fun partial_y_bound => fun partial_y_remainder => fun dy_op_norm => fun dy_inv_op_norm => fun phi_inverse_bound => fun phi_inverse_remainder => fun snd_bound => fun snd_remainder => fun chain_bound => fun chain_remainder => fun evidence => fun x => fun hx => fun h => evidence (@Eq.{w} Y (@ImplicitFunctionDerivativeChainMap.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dPhi_inv_at x h) (@ImplicitFunctionDerivativeFormulaMap.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dFx dFy_inv x h)) (fun (derivative_args_arg : @ImplicitFunctionDerivativeArgs.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dFx dFy dFy_inv dPhi_inv_at target_bound target_remainder partial_x_bound partial_x_remainder partial_y_bound partial_y_remainder dy_op_norm dy_inv_op_norm phi_inverse_bound phi_inverse_remainder snd_bound snd_remainder chain_bound chain_remainder) => fun (basic_evidence_arg : @ImplicitFunctionTheoremEvidence.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder) => fun (differentiability_arg : forall (x : X), forall (hx : x_domain x), @FrechetDifferentiableAt.{u,v,w} Scalar zero one add neg sub mul le_rel X xzero xadd xneg xsmul xnorm Y yzero yadd yneg ysmul ynorm (@ImplicitFunction.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder) x) => fun (derivative_arg : forall (x : X), forall (hx : x_domain x), @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 (@ImplicitFunction.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder) x (@ImplicitFunctionDerivativeChainMap.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dPhi_inv_at x) chain_bound chain_remainder) => fun (formula_arg : forall (x : X), forall (hx : x_domain x), forall (h : X), @Eq.{w} Y (@ImplicitFunctionDerivativeChainMap.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dPhi_inv_at x h) (@ImplicitFunctionDerivativeFormulaMap.{p,q,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 XY xyzero xyadd xyneg xysmul xynorm pairXY fstXY sndXY XZ xzzero xzadd xzneg xzsmul xznorm pairXZ fstXZ sndXZ F base_x base_y x_domain y_domain xy_domain xz_domain phi_inv dPhi dPhi_inv op_norm inv_op_norm inverse_bound inverse_remainder dFx dFy_inv x h)) => formula_arg x hx h)