mathlib3documentation

analysis.calculus.diff_cont_on_cl

Functions differentiable on a domain and continuous on its closure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [ E] [ F] (f : E F) (s : set E) :
Prop
• differentiable_on : s
• continuous_on : (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} [ E] [ F] {f : E F} {s : set E} (h : (closure s)) :
s
theorem differentiable.diff_cont_on_cl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} (h : f) :
s
theorem is_closed.diff_cont_on_cl_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} (hs : is_closed s) :
s s
theorem diff_cont_on_cl_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} :
theorem diff_cont_on_cl_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {s : set E} {c : F} :
(λ (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} [ E] [ F] [ G] {f : E F} {s : set E} {g : G E} {t : set G} (hf : s) (hg : t) (h : t s) :
(f g) t
theorem diff_cont_on_cl.continuous_on_ball {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} [ E] {x : E} {r : } (h : r)) :
r)
theorem diff_cont_on_cl.mk_ball {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {x : E} {r : } (hd : r)) (hc : r)) :
r)
@[protected]
theorem diff_cont_on_cl.differentiable_at {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} {x : E} (h : s) (hs : is_open s) (hx : x s) :
x
theorem diff_cont_on_cl.differentiable_at' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} {x : E} (h : s) (hx : s nhds x) :
x
@[protected]
theorem diff_cont_on_cl.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s t : set E} (h : s) (ht : t s) :
t
theorem diff_cont_on_cl.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f g : E F} {s : set E} (hf : s) (hg : s) :
(f + g) s
theorem diff_cont_on_cl.add_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} (hf : s) (c : F) :
(λ (x : E), f x + c) s
theorem diff_cont_on_cl.const_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} (hf : s) (c : F) :
(λ (x : E), c + f x) s
theorem diff_cont_on_cl.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} (hf : s) :
(-f) s
theorem diff_cont_on_cl.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f g : E F} {s : set E} (hf : s) (hg : s) :
(f - g) s
theorem diff_cont_on_cl.sub_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} (hf : s) (c : F) :
(λ (x : E), f x - c) s
theorem diff_cont_on_cl.const_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} (hf : s) (c : F) :
(λ (x : E), c - f x) s
theorem diff_cont_on_cl.const_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {s : set E} {R : Type u_4} [semiring R] [ F] [ F] (hf : s) (c : R) :
(c f) s
theorem diff_cont_on_cl.smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {𝕜' : Type u_4} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {f : E F} {s : set E} (hc : s) (hf : s) :
(λ (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} [ E] [ F] {𝕜' : Type u_4} [ 𝕜'] [ F] [ 𝕜' F] {c : E 𝕜'} {s : set E} (hc : s) (y : F) :
(λ (x : E), c x y) s
theorem diff_cont_on_cl.inv {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {f : E 𝕜} (hf : s) (h₀ : (x : E), x f x 0) :
s
theorem differentiable.comp_diff_cont_on_cl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ G] {f : E F} {g : G E} {t : set G} (hf : f) (hg : t) :
(f g) t
theorem differentiable_on.diff_cont_on_cl_ball {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E F} {U : set E} {c : E} {R : } (hf : U) (hc : U) :
R)