mathlib documentation

analysis.calculus.diff_on_int_cont

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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_group F] [normed_space π•œ E] [normed_space π•œ F] (f : E β†’ F) (s : set E) :
Prop

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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_group F] [normed_space π•œ E] [normed_space π•œ F] {f : E β†’ F} :
theorem diff_cont_on_cl_const {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_group F] [normed_space π•œ E] [normed_space π•œ F] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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)) :
theorem diff_cont_on_cl.mk_ball {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_group F] [normed_space π•œ E] [normed_space π•œ F] {π•œ' : Type u_4} [nondiscrete_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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_group F] [normed_space π•œ E] [normed_space π•œ F] {π•œ' : Type u_4} [nondiscrete_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} [nondiscrete_normed_field π•œ] [normed_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) :
theorem differentiable.comp_diff_cont_on_cl {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [nondiscrete_normed_field π•œ] [normed_group E] [normed_group F] [normed_space π•œ E] [normed_space π•œ F] [normed_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