Theorem: SubharmonicOn.monotone_lim
Proof state before:
case hf.h_bound.a
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 : ℕ → ℂ → ℝ
g : ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fm : Monotone f
ft : ∀ z ∈ s, Tendsto (fun n => f n z) atTop (𝓝 (g z))
gc : ContinuousOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
sm : ∀ (n : ℕ), f n c ≤ ⨍ (t : ℝ) in itau, f n (circleMap c r t)
r0 : 0 ≤ r
cts : ∀ (t : ℝ), circleMap c r t ∈ s
b' : ℂ → ℝ := fun z => |f 0 z| + |g z|
b : ℝ → ℝ := fun t => b' (circleMap c r t)
bc' : ContinuousOn b' (closedBall c r)
fcc : ∀ (n : ℕ), Continuous fun t => f n (circleMap c r t)
n : ℕ
t : ℝ
a✝ : t ∈ itau
z : ℂ
hz : circleMap c r t = z
zs : z ∈ s
⊢ -b t ≤ f n z ∧ f n z ≤ b t
Tactic:
constructor
Proof state after:
case hf.h_bound.a.left
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 : ℕ → ℂ → ℝ
g : ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fm : Monotone f
ft : ∀ z ∈ s, Tendsto (fun n => f n z) atTop (𝓝 (g z))
gc : ContinuousOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
sm : ∀ (n : ℕ), f n c ≤ ⨍ (t : ℝ) in itau, f n (circleMap c r t)
r0 : 0 ≤ r
cts : ∀ (t : ℝ), circleMap c r t ∈ s
b' : ℂ → ℝ := fun z => |f 0 z| + |g z|
b : ℝ → ℝ := fun t => b' (circleMap c r t)
bc' : ContinuousOn b' (closedBall c r)
fcc : ∀ (n : ℕ), Continuous fun t => f n (circleMap c r t)
n : ℕ
t : ℝ
a✝ : t ∈ itau
z : ℂ
hz : circleMap c r t = z
zs : z ∈ s
⊢ -b t ≤ f n z

case hf.h_bound.a.right
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 : ℕ → ℂ → ℝ
g : ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fm : Monotone f
ft : ∀ z ∈ s, Tendsto (fun n => f n z) atTop (𝓝 (g z))
gc : ContinuousOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
sm : ∀ (n : ℕ), f n c ≤ ⨍ (t : ℝ) in itau, f n (circleMap c r t)
r0 : 0 ≤ r
cts : ∀ (t : ℝ), circleMap c r t ∈ s
b' : ℂ → ℝ := fun z => |f 0 z| + |g z|
b : ℝ → ℝ := fun t => b' (circleMap c r t)
bc' : ContinuousOn b' (closedBall c r)
fcc : ∀ (n : ℕ), Continuous fun t => f n (circleMap c r t)
n : ℕ
t : ℝ
a✝ : t ∈ itau
z : ℂ
hz : circleMap c r t = z
zs : z ∈ s
⊢ f n z ≤ b t