Theorem: HarmonicOn.convex
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ g (⨍ (t_1 : ℝ) in itau, f (circleMap z t t_1)) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Tactic:
apply ConvexOn.map_set_average_le gc c.continuousOn isClosed_univ n.ne_zero n.ne_top
Proof state after:
case intro.intro.hfs
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict itau, f (circleMap z t x) ∈ univ

case intro.intro.hfi
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ IntegrableOn (fun x => f (circleMap z t x)) itau volume

case intro.intro.hgi
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ IntegrableOn (g ∘ fun x => f (circleMap z t x)) itau volume