Documentation

Mathlib.Analysis.Calculus.DiffContOnCl

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} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [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} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [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} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [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} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ๐•œ E] [NormedSpace ๐•œ F] {f : E โ†’ F} {s : Set E} (h : DifferentiableOn ๐•œ f (closure s)) :
    DiffContOnCl ๐•œ f s
    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
    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
    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
    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
    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
    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)) :
    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)
    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
    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
    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 : 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} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [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} [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
    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
    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
    theorem DiffContOnCl.sub {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [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} [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
    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
    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
    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
    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
    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) :
    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
    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)