Functions differentiable on a domain and continuous on its closure #
Many theorems in complex analysis assume that a function is complex differentiable on a domain and
is continuous on its closure. In this file we define a predicate diff_cont_on_cl
that expresses
this property and prove basic facts about this predicate.
structure
diff_cont_on_cl
(π : Type u_1)
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
(f : E β F)
(s : set E) :
Prop
- differentiable_on : differentiable_on π f s
- continuous_on : continuous_on f (closure s)
A predicate saying that a function is differentiable on a set and is continuous on its closure. This is a common assumption in complex analysis.
theorem
differentiable_on.diff_cont_on_cl
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(h : differentiable_on π f (closure s)) :
diff_cont_on_cl π f s
theorem
differentiable.diff_cont_on_cl
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(h : differentiable π f) :
diff_cont_on_cl π f s
theorem
is_closed.diff_cont_on_cl_iff
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(hs : is_closed s) :
diff_cont_on_cl π f s β differentiable_on π f s
theorem
diff_cont_on_cl_univ
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F} :
diff_cont_on_cl π f set.univ β differentiable π f
theorem
diff_cont_on_cl_const
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{s : set E}
{c : F} :
diff_cont_on_cl π (Ξ» (x : E), c) s
theorem
diff_cont_on_cl.comp
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
[normed_add_comm_group G]
[normed_space π G]
{f : E β F}
{s : set E}
{g : G β E}
{t : set G}
(hf : diff_cont_on_cl π f s)
(hg : diff_cont_on_cl π g t)
(h : set.maps_to g t s) :
diff_cont_on_cl π (f β g) t
theorem
diff_cont_on_cl.continuous_on_ball
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
[normed_space β E]
{x : E}
{r : β}
(h : diff_cont_on_cl π f (metric.ball x r)) :
continuous_on f (metric.closed_ball x r)
theorem
diff_cont_on_cl.mk_ball
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{x : E}
{r : β}
(hd : differentiable_on π f (metric.ball x r))
(hc : continuous_on f (metric.closed_ball x r)) :
diff_cont_on_cl π f (metric.ball x r)
@[protected]
theorem
diff_cont_on_cl.differentiable_at
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
{x : E}
(h : diff_cont_on_cl π f s)
(hs : is_open s)
(hx : x β s) :
differentiable_at π f x
theorem
diff_cont_on_cl.differentiable_at'
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
{x : E}
(h : diff_cont_on_cl π f s)
(hx : s β nhds x) :
differentiable_at π f x
@[protected]
theorem
diff_cont_on_cl.mono
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s t : set E}
(h : diff_cont_on_cl π f s)
(ht : t β s) :
diff_cont_on_cl π f t
theorem
diff_cont_on_cl.add
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f g : E β F}
{s : set E}
(hf : diff_cont_on_cl π f s)
(hg : diff_cont_on_cl π g s) :
diff_cont_on_cl π (f + g) s
theorem
diff_cont_on_cl.add_const
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : diff_cont_on_cl π f s)
(c : F) :
diff_cont_on_cl π (Ξ» (x : E), f x + c) s
theorem
diff_cont_on_cl.const_add
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : diff_cont_on_cl π f s)
(c : F) :
diff_cont_on_cl π (Ξ» (x : E), c + f x) s
theorem
diff_cont_on_cl.neg
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : diff_cont_on_cl π f s) :
diff_cont_on_cl π (-f) s
theorem
diff_cont_on_cl.sub
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f g : E β F}
{s : set E}
(hf : diff_cont_on_cl π f s)
(hg : diff_cont_on_cl π g s) :
diff_cont_on_cl π (f - g) s
theorem
diff_cont_on_cl.sub_const
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : diff_cont_on_cl π f s)
(c : F) :
diff_cont_on_cl π (Ξ» (x : E), f x - c) s
theorem
diff_cont_on_cl.const_sub
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
(hf : diff_cont_on_cl π f s)
(c : F) :
diff_cont_on_cl π (Ξ» (x : E), c - f x) s
theorem
diff_cont_on_cl.const_smul
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{f : E β F}
{s : set E}
{R : Type u_4}
[semiring R]
[module R F]
[smul_comm_class π R F]
[has_continuous_const_smul R F]
(hf : diff_cont_on_cl π f s)
(c : R) :
diff_cont_on_cl π (c β’ f) s
theorem
diff_cont_on_cl.smul
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{π' : Type u_4}
[nontrivially_normed_field π']
[normed_algebra π π']
[normed_space π' F]
[is_scalar_tower π π' F]
{c : E β π'}
{f : E β F}
{s : set E}
(hc : diff_cont_on_cl π c s)
(hf : diff_cont_on_cl π f s) :
diff_cont_on_cl π (Ξ» (x : E), c x β’ f x) s
theorem
diff_cont_on_cl.smul_const
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{π' : Type u_4}
[nontrivially_normed_field π']
[normed_algebra π π']
[normed_space π' F]
[is_scalar_tower π π' F]
{c : E β π'}
{s : set E}
(hc : diff_cont_on_cl π c s)
(y : F) :
diff_cont_on_cl π (Ξ» (x : E), c x β’ y) s
theorem
diff_cont_on_cl.inv
{π : Type u_1}
{E : Type u_2}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
{s : set E}
{f : E β π}
(hf : diff_cont_on_cl π f s)
(hβ : β (x : E), x β closure s β f x β 0) :
diff_cont_on_cl π fβ»ΒΉ s
theorem
differentiable.comp_diff_cont_on_cl
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
[normed_add_comm_group G]
[normed_space π G]
{f : E β F}
{g : G β E}
{t : set G}
(hf : differentiable π f)
(hg : diff_cont_on_cl π g t) :
diff_cont_on_cl π (f β g) t