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}
[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
theorem
differentiable_on.diff_cont_on_cl_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}
{U : set E}
{c : E}
{R : ℝ}
(hf : differentiable_on 𝕜 f U)
(hc : metric.closed_ball c R ⊆ U) :
diff_cont_on_cl 𝕜 f (metric.ball c R)