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 DiffContOnCl that expresses this property and prove basic facts about this predicate.

structure DiffContOnCl (๐ : Type u_1) {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] (f : E โ F) (s : Set E) :

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.

Instances For
theorem DiffContOnCl.differentiableOn {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (self : DiffContOnCl ๐ f s) :
DifferentiableOn ๐ f s
theorem DiffContOnCl.continuousOn {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (self : DiffContOnCl ๐ f s) :
theorem DifferentiableOn.diffContOnCl {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (h : DifferentiableOn ๐ f ()) :
DiffContOnCl ๐ f s
theorem Differentiable.diffContOnCl {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (h : Differentiable ๐ f) :
DiffContOnCl ๐ f s
theorem IsClosed.diffContOnCl_iff {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (hs : ) :
DiffContOnCl ๐ f s โ DifferentiableOn ๐ f s
theorem diffContOnCl_univ {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} :
DiffContOnCl ๐ f Set.univ โ Differentiable ๐ f
theorem diffContOnCl_const {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {s : Set E} {c : F} :
DiffContOnCl ๐ (fun (x : E) => c) s
theorem DiffContOnCl.comp {๐ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [] [NormedSpace ๐ E] [NormedSpace ๐ F] [NormedSpace ๐ G] {f : E โ F} {s : Set E} {g : G โ E} {t : Set G} (hf : DiffContOnCl ๐ f s) (hg : DiffContOnCl ๐ g t) (h : Set.MapsTo g t s) :
DiffContOnCl ๐ (f โ g) t
theorem DiffContOnCl.continuousOn_ball {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} [] {x : E} {r : โ} (h : DiffContOnCl ๐ f ()) :
theorem DiffContOnCl.mk_ball {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {x : E} {r : โ} (hd : DifferentiableOn ๐ f ()) (hc : ) :
DiffContOnCl ๐ f ()
theorem DiffContOnCl.differentiableAt {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} {x : E} (h : DiffContOnCl ๐ f s) (hs : ) (hx : x โ s) :
DifferentiableAt ๐ f x
theorem DiffContOnCl.differentiableAt' {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} {x : E} (h : DiffContOnCl ๐ f s) (hx : s โ nhds x) :
DifferentiableAt ๐ f x
theorem DiffContOnCl.mono {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} {t : Set E} (h : DiffContOnCl ๐ f s) (ht : t โ s) :
DiffContOnCl ๐ f t
theorem DiffContOnCl.add {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {g : E โ F} {s : Set E} (hf : DiffContOnCl ๐ f s) (hg : DiffContOnCl ๐ g s) :
DiffContOnCl ๐ (f + g) s
theorem DiffContOnCl.add_const {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (hf : DiffContOnCl ๐ f s) (c : F) :
DiffContOnCl ๐ (fun (x : E) => f x + c) s
theorem DiffContOnCl.const_add {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (hf : DiffContOnCl ๐ f s) (c : F) :
DiffContOnCl ๐ (fun (x : E) => c + f x) s
theorem DiffContOnCl.neg {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (hf : DiffContOnCl ๐ f s) :
DiffContOnCl ๐ (-f) s
theorem DiffContOnCl.sub {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {g : E โ F} {s : Set E} (hf : DiffContOnCl ๐ f s) (hg : DiffContOnCl ๐ g s) :
DiffContOnCl ๐ (f - g) s
theorem DiffContOnCl.sub_const {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (hf : DiffContOnCl ๐ f s) (c : F) :
DiffContOnCl ๐ (fun (x : E) => f x - c) s
theorem DiffContOnCl.const_sub {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} (hf : DiffContOnCl ๐ f s) (c : F) :
DiffContOnCl ๐ (fun (x : E) => c - f x) s
theorem DiffContOnCl.const_smul {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {s : Set E} {R : Type u_5} [] [Module R F] [SMulCommClass ๐ R F] [] (hf : DiffContOnCl ๐ f s) (c : R) :
DiffContOnCl ๐ (c โข f) s
theorem DiffContOnCl.smul {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {๐' : Type u_5} [] [NormedAlgebra ๐ ๐'] [NormedSpace ๐' F] [IsScalarTower ๐ ๐' F] {c : E โ ๐'} {f : E โ F} {s : Set E} (hc : DiffContOnCl ๐ c s) (hf : DiffContOnCl ๐ f s) :
DiffContOnCl ๐ (fun (x : E) => c x โข f x) s
theorem DiffContOnCl.smul_const {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {๐' : Type u_5} [] [NormedAlgebra ๐ ๐'] [NormedSpace ๐' F] [IsScalarTower ๐ ๐' F] {c : E โ ๐'} {s : Set E} (hc : DiffContOnCl ๐ c s) (y : F) :
DiffContOnCl ๐ (fun (x : E) => c x โข y) s
theorem DiffContOnCl.inv {๐ : Type u_1} {E : Type u_2} [] [NormedSpace ๐ E] {s : Set E} {f : E โ ๐} (hf : DiffContOnCl ๐ f s) (hโ : โ x โ , f x โ  0) :
DiffContOnCl ๐ s
theorem Differentiable.comp_diffContOnCl {๐ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [] [NormedSpace ๐ E] [NormedSpace ๐ F] [NormedSpace ๐ G] {f : E โ F} {g : G โ E} {t : Set G} (hf : Differentiable ๐ f) (hg : DiffContOnCl ๐ g t) :
DiffContOnCl ๐ (f โ g) t
theorem DifferentiableOn.diffContOnCl_ball {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [] [NormedSpace ๐ E] [NormedSpace ๐ F] {f : E โ F} {U : Set E} {c : E} {R : โ} (hf : DifferentiableOn ๐ f U) (hc : โ U) :
DiffContOnCl ๐ f ()