# 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.

source
structure DiffContOnCl (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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.

- differentiableOn : DifferentiableOn 𝕜 f s
- continuousOn : ContinuousOn f (closure s)

Instances For

source
theorem DifferentiableOn.diffContOnCl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : DifferentiableOn 𝕜 f (closure s)) :
DiffContOnCl 𝕜 f s
source
theorem Differentiable.diffContOnCl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : Differentiable 𝕜 f) :
DiffContOnCl 𝕜 f s
source
theorem IsClosed.diffContOnCl_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hs : IsClosed s) :
DiffContOnCl 𝕜 f s ↔ DifferentiableOn 𝕜 f s
source
theorem diffContOnCl_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} :
DiffContOnCl 𝕜 f Set.univ ↔ Differentiable 𝕜 f
source
theorem diffContOnCl_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {s : Set E} {c : F} :
DiffContOnCl 𝕜 (fun (x : E) => c) s
source
theorem DiffContOnCl.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [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
source
theorem DiffContOnCl.continuousOn_ball {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} [NormedSpace ℝ E] {x : E} {r : ℝ} (h : DiffContOnCl 𝕜 f (Metric.ball x r)) :
ContinuousOn f (Metric.closedBall x r)
source
theorem DiffContOnCl.mk_ball {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {x : E} {r : ℝ} (hd : DifferentiableOn 𝕜 f (Metric.ball x r)) (hc : ContinuousOn f (Metric.closedBall x r)) :
DiffContOnCl 𝕜 f (Metric.ball x r)
source
theorem DiffContOnCl.differentiableAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (h : DiffContOnCl 𝕜 f s) (hs : IsOpen s) (hx : x ∈ s) :
DifferentiableAt 𝕜 f x
source
theorem DiffContOnCl.differentiableAt' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (h : DiffContOnCl 𝕜 f s) (hx : s ∈ nhds x) :
DifferentiableAt 𝕜 f x
source
theorem DiffContOnCl.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s t : Set E} (h : DiffContOnCl 𝕜 f s) (ht : t ⊆ s) :
DiffContOnCl 𝕜 f t
source
theorem DiffContOnCl.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (hf : DiffContOnCl 𝕜 f s) (hg : DiffContOnCl 𝕜 g s) :
DiffContOnCl 𝕜 (f + g) s
source
theorem DiffContOnCl.add_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : DiffContOnCl 𝕜 f s) (c : F) :
DiffContOnCl 𝕜 (fun (x : E) => f x + c) s
source
theorem DiffContOnCl.const_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : DiffContOnCl 𝕜 f s) (c : F) :
DiffContOnCl 𝕜 (fun (x : E) => c + f x) s
source
theorem DiffContOnCl.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : DiffContOnCl 𝕜 f s) :
DiffContOnCl 𝕜 (-f) s
source
theorem DiffContOnCl.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f g : E → F} {s : Set E} (hf : DiffContOnCl 𝕜 f s) (hg : DiffContOnCl 𝕜 g s) :
DiffContOnCl 𝕜 (f - g) s
source
theorem DiffContOnCl.sub_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : DiffContOnCl 𝕜 f s) (c : F) :
DiffContOnCl 𝕜 (fun (x : E) => f x - c) s
source
theorem DiffContOnCl.const_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hf : DiffContOnCl 𝕜 f s) (c : F) :
DiffContOnCl 𝕜 (fun (x : E) => c - f x) s
source
theorem DiffContOnCl.const_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {R : Type u_5} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (hf : DiffContOnCl 𝕜 f s) (c : R) :
DiffContOnCl 𝕜 (c • f) s
source
theorem DiffContOnCl.smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [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
source
theorem DiffContOnCl.smul_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {s : Set E} (hc : DiffContOnCl 𝕜 c s) (y : F) :
DiffContOnCl 𝕜 (fun (x : E) => c x • y) s
source
theorem DiffContOnCl.inv {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {f : E → 𝕜} (hf : DiffContOnCl 𝕜 f s) (h₀ : ∀ x ∈ closure s, f x ≠ 0) :
DiffContOnCl 𝕜 f⁻¹ s
source
theorem Differentiable.comp_diffContOnCl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {g : G → E} {t : Set G} (hf : Differentiable 𝕜 f) (hg : DiffContOnCl 𝕜 g t) :
DiffContOnCl 𝕜 (f ∘ g) t
source
theorem DifferentiableOn.diffContOnCl_ball {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {U : Set E} {c : E} {R : ℝ} (hf : DifferentiableOn 𝕜 f U) (hc : Metric.closedBall c R ⊆ U) :
DiffContOnCl 𝕜 f (Metric.ball c R)