Functions Harmonic on a Domain and Continuous on Its Closure #
Many theorems in harmonic analysis assume that a function is harmonic on a domain and is continuous
on its closure. In this file we define a predicate HarmonicContOnCl that expresses this property
and prove basic facts about this predicate.
structure
InnerProductSpace.HarmonicContOnCl
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(f : E → F)
(s : Set E)
:
A predicate saying that a function is harmonic on a set and is continuous on its closure. This is a common assumption in harmonic analysis.
- harmonicOnNhd : HarmonicOnNhd f s
- continuousOn : ContinuousOn f (closure s)
Instances For
theorem
InnerProductSpace.HarmonicOnNhd.harmonicContOnCl
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(h : HarmonicOnNhd f (closure s))
:
HarmonicContOnCl f s
theorem
InnerProductSpace.IsClosed.harmonicContOnCl_iff
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hs : IsClosed s)
:
theorem
InnerProductSpace.harmonicContOnCl_const
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{s : Set E}
{c : F}
:
HarmonicContOnCl (fun (x : E) => c) s
theorem
InnerProductSpace.HarmonicContOnCl.continuousOn_ball
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
[NormedSpace ℝ E]
{x : E}
{r : ℝ}
(h : HarmonicContOnCl f (Metric.ball x r))
:
ContinuousOn f (Metric.closedBall x r)
theorem
InnerProductSpace.HarmonicContOnCl.mk_ball
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{x : E}
{r : ℝ}
(hd : HarmonicOnNhd f (Metric.ball x r))
(hc : ContinuousOn f (Metric.closedBall x r))
:
HarmonicContOnCl f (Metric.ball x r)
theorem
InnerProductSpace.HarmonicContOnCl.contDiffAt
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{x : E}
{s : Set E}
(h : HarmonicContOnCl f s)
(hx : x ∈ s)
:
ContDiffAt ℝ 2 f x
theorem
InnerProductSpace.HarmonicContOnCl.differentiableAt
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{x : E}
{s : Set E}
(h : HarmonicContOnCl f s)
(hx : x ∈ s)
:
DifferentiableAt ℝ f x
theorem
InnerProductSpace.HarmonicContOnCl.mono
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s t : Set E}
(h : HarmonicContOnCl f s)
(ht : t ⊆ s)
:
HarmonicContOnCl f t
theorem
InnerProductSpace.HarmonicContOnCl.add
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f₁ f₂ : E → F}
{s : Set E}
(hf₁ : HarmonicContOnCl f₁ s)
(hf₂ : HarmonicContOnCl f₂ s)
:
HarmonicContOnCl (f₁ + f₂) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_add
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f₁ f₂ : E → F}
{s : Set E}
(hf₁ : HarmonicContOnCl f₁ s)
(hf₂ : HarmonicContOnCl f₂ s)
:
HarmonicContOnCl (fun (i : E) => f₁ i + f₂ i) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.add
theorem
InnerProductSpace.HarmonicContOnCl.add_const
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl (f + fun (x : E) => c) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_add_const
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl (fun (i : E) => f i + c) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.add_const
theorem
InnerProductSpace.HarmonicContOnCl.const_add
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl ((fun (x : E) => c) + f) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_const_add
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl (fun (i : E) => c + f i) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.const_add
theorem
InnerProductSpace.HarmonicContOnCl.neg
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
:
HarmonicContOnCl (-f) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_neg
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
:
HarmonicContOnCl (fun (i : E) => -f i) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.neg
theorem
InnerProductSpace.HarmonicContOnCl.sub
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f₁ f₂ : E → F}
{s : Set E}
(hf₁ : HarmonicContOnCl f₁ s)
(hf₂ : HarmonicContOnCl f₂ s)
:
HarmonicContOnCl (f₁ - f₂) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_sub
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f₁ f₂ : E → F}
{s : Set E}
(hf₁ : HarmonicContOnCl f₁ s)
(hf₂ : HarmonicContOnCl f₂ s)
:
HarmonicContOnCl (fun (i : E) => f₁ i - f₂ i) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.sub
theorem
InnerProductSpace.HarmonicContOnCl.sub_const
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl (f - fun (x : E) => c) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_sub_const
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl (fun (i : E) => f i - c) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.sub_const
theorem
InnerProductSpace.HarmonicContOnCl.const_sub
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl ((fun (x : E) => c) - f) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_const_sub
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : F)
:
HarmonicContOnCl (fun (i : E) => c - f i) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.const_sub
theorem
InnerProductSpace.HarmonicContOnCl.const_smul
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : ℝ)
:
HarmonicContOnCl (c • f) s
theorem
InnerProductSpace.HarmonicContOnCl.fun_const_smul
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{F : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : E → F}
{s : Set E}
(hf : HarmonicContOnCl f s)
(c : ℝ)
:
HarmonicContOnCl (fun (i : E) => c • f i) s
Eta-expanded form of InnerProductSpace.HarmonicContOnCl.const_smul