Theory Catalan_Auxiliary_Integral
section ‹Catalan numbers›
theory Catalan_Auxiliary_Integral
imports "HOL-Analysis.Analysis" "HOL-Real_Asymp.Real_Asymp"
begin
subsection ‹Auxiliary integral›
text ‹
First, we will prove the integral $$\int\limits_0^4 \sqrt{\frac{4-x}{x}}\,\textrm{d}x = 2\pi$$
which occurs in the proof for the integral formula for the Catalan numbers.
›
context
begin
text ‹
We prove the integral by explicitly constructing the indefinite integral.
›
lemma catalan_aux_integral:
"((λx::real. sqrt ((4 - x) / x)) has_integral 2 * pi) {0..4}"
proof -
define F where "F ≡ λx. sqrt (4/x - 1) * x - 2 * arctan ((sqrt (4/x - 1) * (x - 2)) / (x - 4))"
define G where "G ≡ λx. if x = 4 then pi else if x = 0 then -pi else F x"
have "(F ⤏ -pi) (at_right 0)"
unfolding F_def by real_asymp
hence G_0: "(G ⤏ -pi) (at_right 0)" unfolding G_def
by (rule Lim_transform_eventually) (auto intro!: eventually_at_rightI[of 0 1])
have "(F ⤏ pi) (at_left 4)"
unfolding F_def by real_asymp
hence G_4: "(G ⤏ pi) (at_left 4)" unfolding G_def
by (rule Lim_transform_eventually) (auto intro!: eventually_at_leftI[of 1])
have deriv_G: "(G has_field_derivative sqrt ((4 - x) / x)) (at x)" if x: "x ∈ {0<..<4}" for x
proof -
from x have "eventually (λy. y ∈ {0<..<4}) (nhds x)"
by (intro eventually_nhds_in_open) simp_all
hence eq: "eventually (λx. F x = G x) (nhds x)" by eventually_elim (simp add: G_def)
define T where "T ≡ λx::real. 4 / (sqrt (4/x - 1) * (x - 4) * x^2)"
have *: "((λx. (sqrt (4/x - 1) * (x - 2)) / (x - 4)) has_field_derivative T x) (at x)"
by (insert x, rule derivative_eq_intros refl | simp)+
(simp add: divide_simps T_def, simp add: field_simps power2_eq_square)
have "((λx. 2 * arctan ((sqrt (4/x - 1) * (x - 2)) / (x - 4))) has_field_derivative
2 * T x / (1 + (sqrt (4 / x - 1) * (x - 2) / (x - 4))⇧2)) (at x)"
by (rule * derivative_eq_intros refl | simp)+ (simp add: field_simps)
also from x have "(sqrt (4 / x - 1) * (x - 2) / (x - 4))⇧2 = (4/x - 1) * (x-2)^2 / (x - 4)^2"
by (simp add: power_mult_distrib power_divide)
also from x have "1 + … = -4 / ((x - 4) * x)"
by (simp add: divide_simps power2_eq_square mult_ac) (simp add: algebra_simps)?
also from x have "2 * T x / … = - (2 / (x * sqrt (4 / x - 1)))"
by (simp add: T_def power2_eq_square)
finally have *: "((λx. 2 * arctan (sqrt (4 / x - 1) * (x - 2) / (x - 4))) has_real_derivative
- (2 / (x * sqrt (4 / x - 1)))) (at x)" .
have "(F has_field_derivative sqrt (4 / x - 1)) (at x)" unfolding F_def
by (insert x, (rule * derivative_eq_intros refl | simp)+) (simp add: field_simps)
thus ?thesis by (subst (asm) DERIV_cong_ev[OF refl eq refl]) (insert x, simp add: field_simps)
qed
have cont_G: "continuous_on {0..4} G" unfolding continuous_on
proof safe
fix x :: real assume "x ∈ {0..4}"
then consider "x = 0" | "x = 4" | "x ∈ {0<..<4}" by force
thus "(G ⤏ G x) (at x within {0..4})"
proof cases
assume "x = 0"
have *: "at (0::real) within {0..4} ≤ at_right 0" unfolding at_within_def
by (rule inf_mono) auto
from G_0 have "(G ⤏ -pi) (at x within {0..4})"
by (rule filterlim_mono) (simp_all add: * ‹x = 0›)
also have "-pi = G x" by (simp add: G_def ‹x = 0›)
finally show ?thesis .
next
assume "x = 4"
have *: "at (4::real) within {0..4} ≤ at_left 4" unfolding at_within_def
by (rule inf_mono) auto
from G_4 have "(G ⤏ pi) (at x within {0..4})"
by (rule filterlim_mono) (simp_all add: * ‹x = 4›)
also have "pi = G x" by (simp add: G_def ‹x = 4›)
finally show ?thesis .
next
assume "x ∈ {0<..<4}"
from deriv_G[OF this] have "isCont G x" by (rule DERIV_isCont)
thus ?thesis unfolding isCont_def by (rule filterlim_mono) (auto simp: at_le)
qed
qed
have "((λx. sqrt ((4 - x) / x)) has_integral G 4 - G 0) {0..4}"
using cont_G deriv_G
by (intro fundamental_theorem_of_calculus_interior)
(auto simp: has_real_derivative_iff_has_vector_derivative)
also have "G 4 - G 0 = 2 * pi" by (simp add: G_def)
finally show ?thesis .
qed
end
end