Theory LogisticFunction
theory LogisticFunction
imports HyperdualFunctionExtension
begin
subsection‹Logistic Function›
text‹Define the standard logistic function and its hyperdual variant:›
definition logistic :: "real ⇒ real"
where "logistic x = inverse (1 + exp (-x))"
definition hyp_logistic :: "real hyperdual ⇒ real hyperdual"
where "hyp_logistic x = inverse (1 + (*h* exp) (-x))"
text‹Hyperdual extension of the logistic function is its hyperdual variant:›
lemma hypext_logistic:
"(*h* logistic) x = hyp_logistic x"
proof -
have "(*h* (λx. exp (- x) + 1)) x = (*h* exp) (- x) + of_comp 1"
by (simp add: hypext_compose hypext_uminus hypext_fun_cadd twice_field_differentiable_at_compose)
then have "(*h* (λx. 1 + exp (- x))) x = 1 + (*h* exp) (- x)"
by (simp add: one_hyperdual_def add.commute)
moreover have "1 + exp (- Base x) ≠ 0"
by (metis exp_ge_zero add_eq_0_iff neg_0_le_iff_le not_one_le_zero)
moreover have "(λx. 1 + exp (- x)) twice_field_differentiable_at Base x"
proof -
have "(λx. exp (- x)) twice_field_differentiable_at Base x"
by (simp add: twice_field_differentiable_at_compose)
then have "(λx. exp (- x) + 1) twice_field_differentiable_at Base x"
using twice_field_differentiable_at_compose[of "λx. exp (- x)" "Base x" "λx. x + 1"]
by simp
then show ?thesis
by (simp add: add.commute)
qed
ultimately have "(*h* (λx. inverse (1 + exp (- x)))) x = inverse (1 + (*h* exp) (- x))"
by (simp add: hypext_fun_inverse)
then show ?thesis
unfolding logistic_def hyp_logistic_def .
qed
text‹From properties of autodiff we know it gives us the derivative:›
lemma "Eps1 (hyp_logistic (β x)) = deriv logistic x"
by (metis Eps1_hypext hypext_logistic)
text‹which is equal to the known derivative of the standard logistic function:›
lemma "First (autodiff logistic x) = exp (- x) / (1 + exp (- x)) ^ 2"
apply (simp only: autodiff.simps hyperdual_to_derivs.simps derivs.sel hypext_logistic)
apply (simp only: hyp_logistic_def inverse_hyperdual.code hyperdual.sel)
apply (simp add: hyperdualx_def hypext_exp_Hyperdual hyperdual_bases)
done
text‹Similarly we can get the second derivative:›
lemma "Second (autodiff logistic x) = deriv (deriv logistic) x"
by (rule autodiff_extract_second)
text‹and derive its value:›
lemma "Second (autodiff logistic x) = ((exp (- x) - 1) * exp (- x)) / ((1 + exp (- x)) ^ 3)"
apply (simp only: autodiff.simps hyperdual_to_derivs.simps derivs.sel hypext_logistic)
apply (simp only: hyp_logistic_def inverse_hyperdual.code hyperdual.sel)
apply (simp add: hyperdualx_def hypext_exp_Hyperdual hyperdual_bases)
proof -
have
"2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x)) ^ 2 =
(2 * exp (- x) / (1 + exp (- x)) ^ 3 - 1 / (1 + exp (- x)) ^ 2) * exp (- x)"
by (simp add: field_simps)
also have "... = (2 * exp (- x) / (1 + exp (- x)) ^ 3 - (1 + exp (- x)) / (1 + exp (- x)) ^ 3) * exp (- x)"
proof -
have "inverse ((1 + exp (- x)) ^ 2) = inverse (1 + exp (- x)) ^ 2"
by (simp add: power_inverse)
also have "... = (1 + exp (- x)) * inverse (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 2"
by (simp add: inverse_eq_divide)
also have "... = (1 + exp (- x)) * inverse (1 + exp (- x)) ^ 3"
by (simp add: power2_eq_square power3_eq_cube)
finally have "inverse ((1 + exp (- x)) ^ 2) = (1 + exp (- x)) * inverse ((1 + exp (- x)) ^ 3)"
by (simp add: power_inverse)
then show ?thesis
by (simp add: inverse_eq_divide)
qed
also have "... = (2 * exp (- x) - (1 + exp (- x))) / (1 + exp (- x)) ^ 3 * exp (- x)"
by (metis diff_divide_distrib)
finally show
"2 * (exp (- x) * exp (- x)) / (1 + exp (- x)) ^ 3 - exp (- x) / (1 + exp (- x))⇧2 =
(exp (- x) - 1) * exp (- x) / (1 + exp (- x)) ^ 3"
by (simp add: field_simps)
qed
end