Theorem: HarmonicOn.convex (Ray/Hartogs/Subharmonic.lean)

State before:
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
⊢ ∀ c ∈ interior s, ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f c) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap c s t))
Tactic:
intro z zs
State after:
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, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))

State before:
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, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior z zs with ⟨r, rp, rh⟩
State after:
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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))

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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Tactic:
exists r, rp
State after:
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
⊢ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))

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
⊢ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Tactic:
intro t tp tr
State after:
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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))

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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Tactic:
have cs : closedBall z t ⊆ s :=
  _root_.trans (Metric.closedBall_subset_ball tr) (_root_.trans rh interior_subset)
State after:
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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))

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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Tactic:
simp only [fh.mean z t tp cs]
State after:
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
⊢ g (⨍ (t_1 : ℝ) in itau, f (circleMap z t t_1)) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))

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
⊢ g (⨍ (t_1 : ℝ) in itau, f (circleMap z t t_1)) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Tactic:
have n := NiceVolume.itau
State after:
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))

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

State before:
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
Tactic:
simp only [Set.mem_univ, Filter.eventually_true]
State after:
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

State before:
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
Tactic:
exact (fh.cont.mono cs).integrableOn_sphere tp
State after:
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

State before:
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
Tactic:
exact ((c.comp_continuousOn fh.cont).mono cs).integrableOn_sphere tp
State after:
no goals