Theory HOL-Analysis.Ck_Implicit_Function
section ‹The ‹C⇧1› inverse and implicit function theorems›
text ‹
‹C⇧1› versions of the inverse and implicit function theorems, and a ‹C⇧k› implicit
function theorem. As in the real-analytic case, the implicit function theorem follows from
the inverse function theorem, applied to ‹Φ (x, y) = (x, F (x, y))›.
›
theory Ck_Implicit_Function
imports Higher_Differentiability_Multi "HOL-Analysis.Determinants"
begin
section ‹From ‹C⇧1› to the inverse-function-theorem interface›
text ‹
The ‹C⇧1› inverse function theorem of HOL-Analysis (‹inverse_function_theorem›)
needs a continuous ‹blinfun›-valued derivative on an open set. We obtain one from
‹Ck_on (Suc 0)›, upgrading continuity of the directional derivatives to continuity in
operator norm.
›
text ‹The Fréchet derivative as a ‹blinfun›.›
definition Dblinfun :: "('a::real_normed_vector ⇒ 'b::real_normed_vector) ⇒ 'a ⇒ ('a ⇒⇩L 'b)"
where "Dblinfun G z = Blinfun (frechet_derivative G (at z))"
lemma blinfun_apply_Dblinfun:
assumes "G differentiable (at z)"
shows "blinfun_apply (Dblinfun G z) = frechet_derivative G (at z)"
proof -
have "bounded_linear (frechet_derivative G (at z))"
using assms frechet_derivative_works has_derivative_bounded_linear by blast
thus ?thesis
unfolding Dblinfun_def by (rule bounded_linear_Blinfun_apply)
qed
text ‹‹C⇧1› at a point: differentiability and continuity of the directional derivatives.›
lemma Ck1_atD:
assumes "Ck_at (Suc 0) G x"
shows "G differentiable (at x)"
and "⋀v. continuous (at x) (λy. frechet_derivative G (at y) v)"
using assms by auto
text ‹From ‹C⇧1› on ‹W›: \<^const>‹Dblinfun› is a derivative of ‹G› on ‹W› and is
continuous there.›
lemma Ck1_on_imp_has_derivative_blinfun:
fixes G :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "Ck_on (Suc 0) G W"
shows "⋀z. z ∈ W ⟹ (G has_derivative blinfun_apply (Dblinfun G z)) (at z)"
proof -
fix z assume z: "z ∈ W"
have "Ck_at (Suc 0) G z"
using assms z by (simp add: Ck_on_def)
hence diff: "G differentiable (at z)" by (rule Ck1_atD)
show "(G has_derivative blinfun_apply (Dblinfun G z)) (at z)"
using diff by (simp add: blinfun_apply_Dblinfun frechet_derivative_works)
qed
lemma Ck1_on_imp_continuous_Dblinfun:
fixes G :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "Ck_on (Suc 0) G W"
shows "continuous_on W (Dblinfun G)"
proof (rule continuous_on_blinfun_componentwise)
fix i :: 'a assume i: "i ∈ Basis"
have W_open: "open W" using assms by (simp add: Ck_on_def)
have cont_dir: "continuous_on W (λz. frechet_derivative G (at z) i)"
proof (rule continuous_at_imp_continuous_on, rule ballI)
fix z assume z: "z ∈ W"
have "Ck_at (Suc 0) G z" using assms z by (simp add: Ck_on_def)
thus "continuous (at z) (λz. frechet_derivative G (at z) i)"
by (rule Ck1_atD(2))
qed
have eq: "⋀z. z ∈ W ⟹ blinfun_apply (Dblinfun G z) i = frechet_derivative G (at z) i"
proof -
fix z assume z: "z ∈ W"
have "Ck_at (Suc 0) G z" using assms z by (simp add: Ck_on_def)
hence "G differentiable (at z)" by (rule Ck1_atD)
thus "blinfun_apply (Dblinfun G z) i = frechet_derivative G (at z) i"
by (simp add: blinfun_apply_Dblinfun)
qed
show "continuous_on W (λz. blinfun_apply (Dblinfun G z) i)"
by (rule continuous_on_eq[OF cont_dir]) (simp add: eq)
qed
text ‹The two halves packaged together.›
theorem Ck1_on_imp_C1_interface:
fixes G :: "'a::euclidean_space ⇒ 'b::euclidean_space"
assumes "Ck_on (Suc 0) G W"
shows "(∀z∈W. (G has_derivative blinfun_apply (Dblinfun G z)) (at z))
∧ continuous_on W (Dblinfun G)"
using Ck1_on_imp_has_derivative_blinfun[OF assms]
Ck1_on_imp_continuous_Dblinfun[OF assms]
by blast
lemma Ck1_on_Pair_fst:
fixes F :: "('a::euclidean_space × 'b::euclidean_space) ⇒ 'b"
assumes C1: "Ck_on (Suc 0) F W"
shows "Ck_on (Suc 0) (λp. (fst p, F p)) W"
unfolding Ck_on_def
proof (intro conjI ballI)
show Wopen: "open W" using C1 by (simp add: Ck_on_def)
fix z assume z: "z ∈ W"
have Fdiff: "F differentiable (at y)" if "y ∈ W" for y
using C1 that by (simp add: Ck_on_def Ck1_atD(1))
have Fcont: "continuous (at y) F" if "y ∈ W" for y
using Fdiff[OF that] by (rule differentiable_imp_continuous_within)
show "Ck_at (Suc 0) (λp. (fst p, F p)) z"
unfolding Ck_at.simps(2)
proof (intro conjI allI)
show "∃A. open A ∧ z ∈ A ∧ (∀y∈A. Ck_at 0 (λp. (fst p, F p)) y)"
proof (intro exI[where x = W] conjI ballI)
fix y assume y: "y ∈ W"
have "continuous (at y) (λp::'a × 'b. (fst p, F p))"
by (intro continuous_intros Fcont[OF y])
thus "Ck_at 0 (λp. (fst p, F p)) y" by simp
qed (use Wopen z in auto)
next
have fst_der: "((fst :: ('a × 'b) ⇒ 'a) has_derivative fst) (at z)"
by (rule bounded_linear.has_derivative[OF bounded_linear_fst has_derivative_ident])
have "(F has_derivative frechet_derivative F (at z)) (at z)"
using Fdiff[OF z] by (rule frechet_derivative_works[THEN iffD1])
from has_derivative_Pair[OF fst_der this]
show "(λp. (fst p, F p)) differentiable (at z)"
unfolding differentiable_def by blast
next
fix v :: "'a × 'b"
have base: "continuous (at z) (λy. (fst v, frechet_derivative F (at y) v))"
using Ck1_atD(2) Ck_on_def assms z by (intro continuous_intros, blast)
have eq: "frechet_derivative (λp. (fst p, F p)) (at y) v
= (fst v, frechet_derivative F (at y) v)" if "y ∈ W" for y
by (simp add: frechet_derivative_Pair_fst[OF Fdiff[OF that]])
obtain d :: real where dpos: "0 < d" and dball: "ball z d ⊆ W"
using Wopen z by (metis openE)
have base': "continuous (at z within UNIV)
(λy. (fst v, frechet_derivative F (at y) v))"
using base by simp
have "continuous (at z within UNIV)
(λy. frechet_derivative (λp. (fst p, F p)) (at y) v)"
proof (rule continuous_transform_within [OF base' dpos UNIV_I])
fix y :: "'a × 'b" assume "y ∈ UNIV" and "dist y z < d"
hence "y ∈ W"
by (metis dball dist_commute in_mono mem_ball)
thus "(fst v, frechet_derivative F (at y) v)
= frechet_derivative (λp. (fst p, F p)) (at y) v"
by (simp only: eq)
qed
thus "Ck_at 0 (λy. frechet_derivative (λp. (fst p, F p)) (at y) v) z"
by simp
qed
qed
subsection ‹The ‹C⇧1› local inverse›
text ‹
The inverse function theorem of HOL-Analysis needs a continuous ‹blinfun›-valued
derivative (@{thm [source] Ck1_on_imp_C1_interface}) and a left inverse of the derivative at ‹z⇩0›,
here ‹Blinfun (inv B)›.
›
theorem C1_local_inverse:
fixes G :: "'a::euclidean_space ⇒ 'a"
assumes C1: "Ck_on (Suc 0) G W"
and pW: "z0 ∈ W"
and reg: "∃B. (G has_derivative B) (at z0) ∧ bij B"
obtains U' V H where
"open U'" and "z0 ∈ U'" and "U' ⊆ W"
and "open V" and "G z0 ∈ V"
and "homeomorphism U' V G H"
and "⋀y. y ∈ V ⟹ H differentiable (at y)"
proof -
have Wopen: "open W" using C1 by (simp add: Ck_on_def)
obtain B where Bder: "(G has_derivative B) (at z0)" and bijB: "bij B"
using reg by blast
have derG: "⋀z. z ∈ W ⟹ (G has_derivative blinfun_apply (Dblinfun G z)) (at z)"
by (rule Ck1_on_imp_has_derivative_blinfun[OF C1])
have contG: "continuous_on W (Dblinfun G)"
by (rule Ck1_on_imp_continuous_Dblinfun[OF C1])
have Beq: "blinfun_apply (Dblinfun G z0) = B"
by (rule has_derivative_unique[OF derG[OF pW] Bder])
have blB: "bounded_linear B" using Bder by (rule has_derivative_bounded_linear)
have injB: "inj B" using bijB by (simp add: bij_def)
have blinvB: "bounded_linear (inv B)"
by (rule inj_linear_imp_inv_bounded_linear[OF blB injB])
have applyinv: "blinfun_apply (Blinfun (inv B)) = inv B"
by (rule bounded_linear_Blinfun_apply[OF blinvB])
have invf: "Blinfun (inv B) o⇩L Dblinfun G z0 = id_blinfun"
proof (rule blinfun_eqI)
fix i
have "blinfun_apply (Blinfun (inv B) o⇩L Dblinfun G z0) i = inv B (B i)"
by (simp add: applyinv Beq)
also have "… = i" using injB by (simp add: inv_f_f)
finally show "blinfun_apply (Blinfun (inv B) o⇩L Dblinfun G z0) i
= blinfun_apply id_blinfun i" by simp
qed
obtain U' V H H' where
U'open: "open U'" and U'sub: "U' ⊆ W" and z0U': "z0 ∈ U'"
and Vopen: "open V" and GzV: "G z0 ∈ V"
and homeo: "homeomorphism U' V G H"
and Hder: "⋀y. y ∈ V ⟹ (H has_derivative (H' y)) (at y)"
and H'eq: "⋀y. y ∈ V ⟹ H' y = inv (blinfun_apply (Dblinfun G (H y)))"
and Hbij: "⋀y. y ∈ V ⟹ bij (blinfun_apply (Dblinfun G (H y)))"
by (rule inverse_function_theorem[OF Wopen derG contG pW invf], simp_all)
have Hdiff: "H differentiable (at y)" if "y ∈ V" for y
using Hder[OF that] unfolding differentiable_def by blast
show ?thesis
by (rule that[OF U'open z0U' U'sub Vopen GzV homeo Hdiff])
qed
subsection ‹The ‹C⇧1› implicit function theorem›
text ‹The implicit function theorem for ‹C⇧1› data; the solution map is differentiable.›
theorem C1_implicit_function:
fixes F :: "('a::euclidean_space × 'b::euclidean_space) ⇒ 'b"
assumes C1: "Ck_on (Suc 0) F W"
and pW: "(x0, y0) ∈ W"
and F0: "F (x0, y0) = 0"
and reg: "∃L. ((λy. F (x0, y)) has_derivative L) (at y0) ∧ bij L"
obtains U g where
"open U" and "x0 ∈ U" and "g x0 = y0"
and "⋀x. x ∈ U ⟹ g differentiable (at x)"
and "∀x∈U. (x, g x) ∈ W ∧ F (x, g x) = 0"
proof -
have Wopen: "open W" using C1 by (simp add: Ck_on_def)
let ?Phi = "λp::'a × 'b. (fst p, F p)"
let ?p0 = "(x0, y0)"
obtain L where Lder: "((λy. F (x0, y)) has_derivative L) (at y0)"
and bijL: "bij L" using reg by blast
have Phi_C1: "Ck_on (Suc 0) ?Phi W" by (rule Ck1_on_Pair_fst[OF C1])
have Fdiff: "F differentiable (at ?p0)"
using C1 pW by (simp add: Ck_on_def Ck1_atD(1))
then obtain A where Fder: "(F has_derivative A) (at ?p0)"
unfolding differentiable_def by blast
have slice_der: "((λy. F (x0, y)) has_derivative (λdy. A (0, dy))) (at y0)"
proof -
have pair_der: "((λy. (x0, y)) has_derivative (λdy. (0, dy))) (at y0)"
proof -
have cder: "((λy::'b. x0) has_derivative (λdy. 0)) (at y0)"
by (rule has_derivative_const)
have idder: "((λy::'b. y) has_derivative (λdy. dy)) (at y0)"
by (rule has_derivative_ident)
show ?thesis using has_derivative_Pair[OF cder idder] by simp
qed
show ?thesis using has_derivative_compose[OF pair_der Fder] by simp
qed
have L_eq: "L = (λdy. A (0, dy))"
by (rule has_derivative_unique[OF Lder slice_der])
let ?B = "λh::'a × 'b. (fst h, A h)"
have Phi_der: "(?Phi has_derivative ?B) (at ?p0)"
proof -
have fst_der: "((fst :: ('a × 'b) ⇒ 'a) has_derivative fst) (at ?p0)"
by (rule bounded_linear.has_derivative[OF bounded_linear_fst has_derivative_ident])
show ?thesis using has_derivative_Pair[OF fst_der Fder] by simp
qed
have blA: "bounded_linear A" using Fder by (rule has_derivative_bounded_linear)
interpret A: bounded_linear A by (rule blA)
have surjL: "surj L" and injL: "inj L" using bijL by (auto simp: bij_def)
let ?C = "λq::'a × 'b. (fst q, inv L (snd q - A (fst q, 0)))"
have B_C: "?B (?C q) = q" for q
proof -
let ?w = "snd q - A (fst q, 0)"
have decomp: "(fst q, inv L ?w) = (fst q, 0) + (0, inv L ?w)" by simp
have Aq: "A (fst q, inv L ?w) = A (fst q, 0) + A (0, inv L ?w)"
by (subst decomp) (rule A.add)
have A0_inv: "A (0, inv L ?w) = ?w"
proof -
have "A (0, inv L ?w) = L (inv L ?w)" using L_eq by simp
also have "... = ?w" using surjL by (rule surj_f_inv_f)
finally show ?thesis .
qed
have "A (fst q, inv L ?w) = snd q" using Aq A0_inv by simp
thus ?thesis by simp
qed
have C_B: "?C (?B h) = h" for h
proof -
have decomp: "h = (fst h, 0) + (0, snd h)" by simp
have Ah: "A h = A (fst h, 0) + A (0, snd h)"
by (subst decomp) (rule A.add)
have "A h - A (fst h, 0) = L (snd h)" using Ah L_eq by simp
thus ?thesis using injL by (simp add: inv_f_f)
qed
have bijB: "bij ?B"
proof (rule bijI)
show "inj ?B"
proof (rule injI)
fix u v :: "'a × 'b"
assume "?B u = ?B v"
hence "?C (?B u) = ?C (?B v)" by simp
thus "u = v" using C_B by metis
qed
show "surj ?B"
unfolding surj_def using B_C by metis
qed
obtain U' V Psi where U'open: "open U'" and p0U': "?p0 ∈ U'"
and U'sub: "U' ⊆ W" and Vopen: "open V"
and PhiV: "?Phi ?p0 ∈ V"
and homeo: "homeomorphism U' V ?Phi Psi"
and Psi_diff: "⋀q. q ∈ V ⟹ Psi differentiable (at q)"
by (rule C1_local_inverse[OF Phi_C1 pW]) (use Phi_der bijB in blast)+
define U where "U = {x. (x, 0::'b) ∈ V}"
define g where "g = (λx. snd (Psi (x, 0::'b)))"
have Uopen: "open U"
proof -
have "continuous_on UNIV (λx::'a. (x, 0::'b))" by (intro continuous_intros)
from continuous_open_preimage[OF this open_UNIV Vopen]
show ?thesis by (simp add: U_def vimage_def)
qed
have x0U: "x0 ∈ U" using PhiV F0 by (simp add: U_def)
have gx0: "g x0 = y0"
using homeomorphism_apply1[OF homeo p0U'] F0 by (simp add: g_def)
have gdiff: "g differentiable (at x)" if xU: "x ∈ U" for x
proof -
have slice: "((λx::'a. (x, 0::'b)) has_derivative (λdx. (dx, 0::'b))) (at x)"
proof -
have idder: "((λx::'a. x) has_derivative (λdx. dx)) (at x)"
by (rule has_derivative_ident)
have cder: "((λx::'a. 0::'b) has_derivative (λdx. 0)) (at x)"
by (rule has_derivative_const)
show ?thesis using has_derivative_Pair[OF idder cder] by simp
qed
have inV: "(x, 0::'b) ∈ V" using xU by (simp add: U_def)
obtain P where P: "(Psi has_derivative P) (at (x, 0::'b))"
using Psi_diff[OF inV] unfolding differentiable_def by blast
have "((λx::'a. Psi (x, 0::'b)) has_derivative (λdx. P (dx, 0))) (at x)"
using has_derivative_compose[OF slice P] by simp
from bounded_linear.has_derivative[OF bounded_linear_snd this]
show ?thesis unfolding g_def differentiable_def by blast
qed
have solution: "∀x∈U. (x, g x) ∈ W ∧ F (x, g x) = 0"
proof
fix x assume xU: "x ∈ U"
have inV: "(x, 0::'b) ∈ V" using xU by (simp add: U_def)
have Psi_in: "Psi (x, 0::'b) ∈ U'"
using homeomorphism_image2[OF homeo] inV by blast
have PhiPsi: "?Phi (Psi (x, 0::'b)) = (x, 0::'b)"
by (rule homeomorphism_apply2[OF homeo inV])
have "(x, g x) = Psi (x, 0::'b)"
using PhiPsi by (simp add: g_def prod_eq_iff)
thus "(x, g x) ∈ W ∧ F (x, g x) = 0"
using Psi_in U'sub PhiPsi by auto
qed
show ?thesis by (rule that[OF Uopen x0U gx0 gdiff solution])
qed
subsection ‹Further ‹C⇧k› closure properties›
text ‹
Closure properties for bootstrapping from ‹C⇧1› to ‹C⇧k›: vectors with ‹C⇧k›
components, finite products and determinants.
›
lemma Ck_on_scaleR_right:
fixes s :: "'a::real_normed_vector ⇒ real"
assumes "Ck_on k s U"
shows "Ck_on k (λy. s y *⇩R v) U"
by (rule Ck_on_bounded_linear_compose[OF bounded_linear_scaleR_left assms])
lemma Ck_on_vec:
fixes f :: "'a::real_normed_vector ⇒ real^'n::finite"
assumes oU: "open U" and comps: "⋀r. Ck_on k (λy. f y $ r) U"
shows "Ck_on k f U"
proof -
have "Ck_on k (λy. ∑r∈(UNIV::'n set). (f y $ r) *⇩R axis r 1) U"
by (rule Ck_on_sum, simp_all, simp only: Ck_on_scaleR_right comps)
thus ?thesis
by (metis (no_types, lifting) ext basis_expansion scalar_mult_eq_scaleR)
qed
text ‹Finite products, and hence determinants of matrices with ‹C⇧k› entries.›
lemma Ck_on_prod:
fixes f :: "'i ⇒ 'a::real_normed_vector ⇒ real"
assumes fin: "finite I" and oU: "open U"
and Ck: "⋀i. i ∈ I ⟹ Ck_on k (f i) U"
shows "Ck_on k (λy. ∏i∈I. f i y) U"
using fin Ck
proof (induction rule: finite_induct)
case empty
show ?case using oU by (simp add: Ck_on_const)
next
case (insert i I)
have "Ck_on k (λy. f i y * (∏j∈I. f j y)) U"
by (rule Ck_on_mult[OF insert.prems[of i] insert.IH]) (use insert.prems in auto)
thus ?case using insert.hyps by simp
qed
lemma Ck_on_det:
fixes M :: "'a::real_normed_vector ⇒ real^'n::finite^'n"
assumes oU: "open U"
and Ck: "⋀i j. Ck_on k (λy. M y $ i $ j) U"
shows "Ck_on k (λy. det (M y)) U"
proof -
have finP: "finite {p. p permutes (UNIV::'n set)}" by (simp add: finite_permutations)
have neP: "{p. p permutes (UNIV::'n set)} ≠ {}"
using permutes_id by blast
have term_Ck: "Ck_on k (λy. of_int (sign p) * (∏i∈UNIV. M y $ i $ p i)) U"
for p :: "'n ⇒ 'n"
proof (rule Ck_on_mult)
show "Ck_on k (λy. of_int (sign p) :: real) U" using oU by (rule Ck_on_const)
show "Ck_on k (λy. ∏i∈(UNIV::'n set). M y $ i $ p i) U"
using assms by (subst Ck_on_prod, simp_all)
qed
have "Ck_on k (λy. ∑p | p permutes (UNIV::'n set).
of_int (sign p) * (∏i∈UNIV. M y $ i $ p i)) U"
by (rule Ck_on_sum[OF finP neP]) (use term_Ck in blast)
thus ?thesis by (simp only: det_def)
qed
subsection ‹Cramer: a linear system with ‹C⇧k› data has a ‹C⇧k› solution›
text ‹
If the matrix and right-hand side of a linear system are ‹C⇧k› in a parameter and the
matrix stays nonsingular, then the solution is ‹C⇧k› (by Cramer's rule).
›
lemma Ck_on_solve_linear:
fixes M :: "'a::real_normed_vector ⇒ real^'n::finite^'n"
and b w :: "'a ⇒ real^'n"
assumes oU: "open U"
and MC: "⋀i j. Ck_on k (λy. M y $ i $ j) U"
and bC: "⋀i. Ck_on k (λy. b y $ i) U"
and nz: "⋀y. y ∈ U ⟹ det (M y) ≠ 0"
and sol: "⋀y. y ∈ U ⟹ M y *v w y = b y"
shows "Ck_on k w U"
proof (rule Ck_on_vec[OF oU])
fix r
have comp: "w y $ r = det (χ i j. if j = r then b y $ i else M y $ i $ j) / det (M y)"
if yU: "y ∈ U" for y
proof -
have "w y = (χ t. det (χ i j. if j = t then b y $ i else M y $ i $ j) / det (M y))"
using cramer[OF nz[OF yU]] sol[OF yU] by blast
thus ?thesis by simp
qed
have numC: "Ck_on k (λy. det (χ i j. if j = r then b y $ i else M y $ i $ j)) U"
proof (rule Ck_on_det[OF oU])
fix i j
show "Ck_on k (λy. (χ i j. if j = r then b y $ i else M y $ i $ j) $ i $ j) U"
by (cases "j = r") (simp_all add: bC MC)
qed
have denC: "Ck_on k (λy. det (M y)) U" by (rule Ck_on_det[OF oU MC])
have "Ck_on k (λy. det (χ i j. if j = r then b y $ i else M y $ i $ j) / det (M y)) U"
by (rule Ck_on_divide[OF numC denC]) (use nz in blast)
thus "Ck_on k (λy. w y $ r) U"
by (rule Ck_on_congI) (simp add: comp)
qed
subsection ‹The ‹C⇧k› implicit function theorem›
text ‹
Starting from @{thm [source] C1_implicit_function}, differentiating ‹F (x, g x) = 0› gives
a linear system for the derivative of ‹g›, whose matrix is nonsingular near ‹x⇩0›. If
‹g› is ‹C⇧j›, then so are the data of the system and hence, by
@{thm [source] Ck_on_solve_linear}, the derivative of ‹g›; induction on ‹j› gives ‹C⇧k›.
The unknown ranges over ‹real^'n› so that Cramer's rule applies.
›
theorem Ck_implicit_function:
fixes F :: "('a::euclidean_space × (real^'n::finite)) ⇒ real^'n"
assumes Ck: "Ck_on k F W"
and k1: "1 ≤ k"
and pW: "(x0, y0) ∈ W"
and F0: "F (x0, y0) = 0"
and reg: "∃L. ((λy. F (x0, y)) has_derivative L) (at y0) ∧ bij L"
obtains U g where
"open U" and "x0 ∈ U" and "g x0 = y0"
and "Ck_on k g U"
and "∀x∈U. (x, g x) ∈ W ∧ F (x, g x) = 0"
proof -
have Wopen: "open W" using Ck by (simp add: Ck_on_def)
obtain m where km: "k = Suc m" using k1 by (cases k) auto
have C1: "Ck_on (Suc 0) F W" by (rule Ck_on_mono[OF Ck]) (use k1 in simp)
text ‹The ‹C⇧1› theorem supplies the solution map.›
obtain U0 g where U0open: "open U0" and x0U0: "x0 ∈ U0" and gx0: "g x0 = y0"
and gdiff: "⋀x. x ∈ U0 ⟹ g differentiable (at x)"
and gsol: "∀x∈U0. (x, g x) ∈ W ∧ F (x, g x) = 0"
by (rule C1_implicit_function[OF C1 pW F0 reg]) blast
text ‹The derivative of ‹F› along the graph, and its second-slot matrix.›
define DF where "DF = (λx. frechet_derivative F (at (x, g x)))"
define M where "M = (λx. (χ i j. DF x (0, axis j 1) $ i))"
have Fdiff: "F differentiable (at q)" if "q ∈ W" for q
proof -
have "Ck_at (Suc 0) F q" using C1 that by (simp add: Ck_on_def)
thus ?thesis by (rule Ck1_atD(1))
qed
have blDF: "bounded_linear (DF x)" if "x ∈ U0" for x
proof -
have "(x, g x) ∈ W" using gsol that by blast
from Fdiff[OF this] show ?thesis
unfolding DF_def
by (metis frechet_derivative_works has_derivative_bounded_linear)
qed
have Mworks: "M x *v w = DF x (0, w)" if xU0: "x ∈ U0" for x w
proof -
have lin: "linear (λw. DF x (0, w))"
proof -
interpret D: bounded_linear "DF x" by (rule blDF[OF xU0])
show ?thesis
proof (rule linearI)
fix u v :: "real^'n"
show "DF x (0, u + v) = DF x (0, u) + DF x (0, v)"
using D.add[of "(0, u)" "(0, v)"] by simp
next
fix c :: real and u :: "real^'n"
show "DF x (0, c *⇩R u) = c *⇩R DF x (0, u)"
using D.scaleR[of c "(0, u)"] by simp
qed
qed
have "M x = matrix (λw. DF x (0, w))" by (simp add: M_def matrix_def)
thus ?thesis using lin by (simp add: matrix_works)
qed
text ‹At ‹x⇩0› the matrix is the one that ‹reg› makes invertible.›
have detx0: "det (M x0) ≠ 0"
proof -
obtain L where Lder: "((λy. F (x0, y)) has_derivative L) (at y0)" and bijL: "bij L"
using reg by blast
have slice: "((λy. F (x0, y)) has_derivative (λdy. DF x0 (0, dy))) (at y0)"
proof -
have c: "((λy::real^'n. x0) has_derivative (λdy. 0)) (at y0)"
by (rule has_derivative_const)
have i: "((λy::real^'n. y) has_derivative (λdy. dy)) (at y0)"
by (rule has_derivative_ident)
have pd: "((λy. (x0, y)) has_derivative (λdy. (0, dy))) (at y0)"
using has_derivative_Pair[OF c i] by simp
have "(F has_derivative DF x0) (at (x0, g x0))"
unfolding DF_def using Fdiff[OF pW] gx0
by (simp add: frechet_derivative_works)
hence Fd: "(F has_derivative DF x0) (at (x0, y0))" by (simp add: gx0)
from has_derivative_compose[OF pd Fd] show ?thesis by simp
qed
have Leq: "L = (λdy. DF x0 (0, dy))" by (rule has_derivative_unique[OF Lder slice])
have linL: "linear L" using Lder by (rule has_derivative_linear)
have "inj L" using bijL by (simp add: bij_def)
hence "det (matrix L) ≠ 0" using linL by (simp add: det_nz_iff_inj)
moreover have "matrix L = M x0" by (simp add: Leq M_def matrix_def)
ultimately show ?thesis by simp
qed
text ‹Shrink to the set where the matrix stays nonsingular.›
have contM: "continuous_on U0 (λx. det (M x))"
proof -
have ent: "continuous_on U0 (λx. M x $ i $ j)" for i j
proof (rule continuous_at_imp_continuous_on, rule ballI)
fix x assume x: "x ∈ U0"
have gc: "isCont g x"
using gdiff[OF x] by (simp add: differentiable_imp_continuous_within)
have pair: "isCont (λx. (x, g x)) x"
by (intro continuous_intros gc)
have inW: "(x, g x) ∈ W" using gsol x by blast
have "Ck_at (Suc 0) F (x, g x)" using C1 inW by (simp add: Ck_on_def)
hence cd: "isCont (λq. frechet_derivative F (at q) (0, axis j 1)) (x, g x)"
by (rule Ck1_atD(2))
have "isCont ((λq. frechet_derivative F (at q) (0, axis j 1)) ∘ (λx. (x, g x))) x"
by (rule continuous_at_compose[OF pair cd])
hence "isCont (λx. DF x (0, axis j 1)) x" by (simp add: o_def DF_def)
hence "isCont (λx. DF x (0, axis j 1) $ i) x"
by (rule bounded_linear.continuous[OF bounded_linear_vec_nth])
thus "isCont (λx. M x $ i $ j) x" by (simp add: M_def)
qed
show ?thesis
unfolding det_def
by (intro continuous_on_sum continuous_on_mult continuous_on_const
continuous_on_prod ent)
qed
define U where "U = U0 ∩ {x. det (M x) ≠ 0}"
have Uopen: "open U"
proof -
have "open ((λx. det (M x)) -` (- {0}) ∩ U0)"
using continuous_on_open_vimage[OF U0open] contM by blast
moreover have "(λx. det (M x)) -` (- {0}) ∩ U0 = U" by (auto simp: U_def)
ultimately show ?thesis by simp
qed
have x0U: "x0 ∈ U" using x0U0 detx0 by (simp add: U_def)
have UsubU0: "U ⊆ U0" by (simp add: U_def)
have detU: "det (M x) ≠ 0" if "x ∈ U" for x using that by (simp add: U_def)
text ‹The linear system satisfied by the derivative of ‹g›.›
have gsys: "M x *v (frechet_derivative g (at x) u) = - DF x (u, 0)"
if xU: "x ∈ U" for x u
proof -
have xU0: "x ∈ U0" using xU UsubU0 by blast
have inW: "(x, g x) ∈ W" using gsol xU0 by blast
have Fd: "(F has_derivative DF x) (at (x, g x))"
unfolding DF_def using Fdiff[OF inW] by (simp add: frechet_derivative_works)
have gd: "(g has_derivative frechet_derivative g (at x)) (at x)"
using gdiff[OF xU0] by (simp add: frechet_derivative_works)
have idd: "((λx::'a. x) has_derivative (λh. h)) (at x)" by (rule has_derivative_ident)
have graph: "((λx. (x, g x)) has_derivative
(λh. (h, frechet_derivative g (at x) h))) (at x)"
using has_derivative_Pair[OF idd gd] by simp
have comp: "((λx. F (x, g x)) has_derivative
(λh. DF x (h, frechet_derivative g (at x) h))) (at x)"
using has_derivative_compose[OF graph Fd] by simp
have zero: "((λx. F (x, g x)) has_derivative (λh. 0)) (at x)"
proof (rule has_derivative_transform_within_open[where f = "λ_. 0" and s = U0])
show "((λ_::'a. 0::real^'n) has_derivative (λh. 0)) (at x)"
by (rule has_derivative_const)
show "open U0" by (rule U0open)
show "x ∈ U0" by (rule xU0)
show "⋀y. y ∈ U0 ⟹ (0::real^'n) = F (y, g y)" using gsol by auto
qed
have vanish: "DF x (u, frechet_derivative g (at x) u) = 0"
using fun_cong[OF has_derivative_unique[OF comp zero], of u] by simp
have split: "DF x (u, frechet_derivative g (at x) u)
= DF x (u, 0) + DF x (0, frechet_derivative g (at x) u)"
proof -
interpret D: bounded_linear "DF x" by (rule blDF[OF xU0])
have "(u, frechet_derivative g (at x) u)
= (u, 0) + (0, frechet_derivative g (at x) u)" by simp
thus ?thesis by (metis D.add)
qed
from vanish split have "DF x (0, frechet_derivative g (at x) u) = - DF x (u, 0)"
by (metis add_eq_0_iff)
thus ?thesis using Mworks[OF xU0] by simp
qed
text ‹Regularity of the coefficients, given regularity of ‹g›.›
have dFCk: "Ck_on j (λx. DF x u) U" if gj: "Ck_on j g U" and jm: "j ≤ m" for j u
proof -
have innerm: "Ck_on m (λq. frechet_derivative F (at q) u) W"
unfolding Ck_on_def
proof (intro conjI ballI)
show "open W" by (rule Wopen)
fix q assume q: "q ∈ W"
have "Ck_at (Suc m) F q" using Ck q km by (simp add: Ck_on_def)
thus "Ck_at m (λq'. frechet_derivative F (at q') u) q"
by (simp only: Ck_at.simps(2))
qed
have inner: "Ck_on j (λq. frechet_derivative F (at q) u) W"
by (rule Ck_on_mono[OF innerm jm])
have graph: "Ck_on j (λx. (x, g x)) U"
by (rule Ck_on_Pair[OF Ck_on_id[OF Uopen] gj])
have img: "⋀x. x ∈ U ⟹ (x, g x) ∈ W" using gsol UsubU0 by blast
show ?thesis
unfolding DF_def by (rule Ck_on_compose[OF inner graph img])
qed
text ‹The bootstrap induction.›
have boot: "j ≤ k ⟹ Ck_on j g U" for j
proof (induction j)
case 0
show ?case
unfolding Ck_on_def
proof (intro conjI ballI)
show "open U" by (rule Uopen)
fix x assume x: "x ∈ U"
have "continuous (at x) g"
using gdiff[OF UsubU0[THEN subsetD, OF x]]
by (simp add: differentiable_imp_continuous_within)
thus "Ck_at 0 g x" by simp
qed
next
case (Suc j)
have jk: "j ≤ k" using Suc.prems by simp
have jm: "j ≤ m" using Suc.prems km by simp
have IH: "Ck_on j g U" by (rule Suc.IH[OF jk])
have derCk: "Ck_on j (λx. frechet_derivative g (at x) u) U" for u
proof (rule Ck_on_solve_linear[OF Uopen])
fix i jj
have "Ck_on j (λx. DF x (0, axis jj 1) $ i) U"
by (rule Ck_on_component[OF dFCk[OF IH jm]])
thus "Ck_on j (λx. M x $ i $ jj) U" by (simp add: M_def)
next
fix i
have "Ck_on j (λx. DF x (u, 0)) U" by (rule dFCk[OF IH jm])
hence "Ck_on j (λx. - DF x (u, 0)) U" by (rule Ck_on_neg)
thus "Ck_on j (λx. (- DF x (u, 0)) $ i) U" by (rule Ck_on_component)
next
show "⋀x. x ∈ U ⟹ det (M x) ≠ 0" by (rule detU)
next
show "⋀x. x ∈ U ⟹ M x *v frechet_derivative g (at x) u = - DF x (u, 0)"
by (rule gsys)
qed
show ?case
unfolding Ck_on_def
proof (intro conjI ballI)
show "open U" by (rule Uopen)
fix x assume x: "x ∈ U"
show "Ck_at (Suc j) g x"
unfolding Ck_at.simps(2)
proof (intro conjI allI)
show "∃A. open A ∧ x ∈ A ∧ (∀y∈A. Ck_at j g y)"
using Uopen x IH by (auto simp: Ck_on_def)
show "g differentiable (at x)" by (rule gdiff[OF UsubU0[THEN subsetD, OF x]])
fix v
show "Ck_at j (λy. frechet_derivative g (at y) v) x"
using derCk[of v] x by (simp add: Ck_on_def)
qed
qed
qed
have solU: "∀x∈U. (x, g x) ∈ W ∧ F (x, g x) = 0" using gsol UsubU0 by blast
show ?thesis
by (rule that[OF Uopen x0U gx0 boot[OF order_refl] solU])
qed
end