Theorem: SubharmonicOn.monotone_lim
Proof state before:
case hf
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)
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
Tactic:
apply tendsto_integral_of_dominated_convergence b
Proof state after:
case hf.F_measurable
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 : ℕ), AEStronglyMeasurable (fun a => f n (circleMap c r a)) (volume.restrict itau)

case hf.bound_integrable
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)
⊢ Integrable b (volume.restrict itau)

case hf.h_bound
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 : ℕ), ∀ᵐ (a : ℝ) ∂volume.restrict itau, ‖f n (circleMap c r a)‖ ≤ b a

case hf.h_lim
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)
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict itau, Tendsto (fun n => f n (circleMap c r a)) atTop (𝓝 (g (circleMap c r a)))