internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.partialSups
Proof state before:
case zero
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 : ℕ → ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
⊢ SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) 0) s
Tactic:
simp only [fs 0, partialSups_zero]
Proof state after:
no goals
Theorem: SubharmonicOn.partialSups
Proof state before:
case succ
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 : ℕ → ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
n : ℕ
h : SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) n) s
⊢ SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) (n + 1)) s
Tactic:
simp only [partialSups_succ]
Proof state after:
case succ
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 : ℕ → ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
n : ℕ
h : SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) n) s
⊢ SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) n ⊔ f (n + 1) z) s
Theorem: SubharmonicOn.partialSups
Proof state before:
case succ
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 : ℕ → ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
n : ℕ
h : SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) n) s
⊢ SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) n ⊔ f (n + 1) z) s
Tactic:
exact h.max (fs (n + 1))
Proof state after:
no goals
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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
⊢ SubharmonicOn g s
Tactic:
rw [subharmonicOn_iff_submean gc]
Proof 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 : ℕ → ℂ → ℝ
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 > 0, closedBall c r ⊆ s → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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 > 0, closedBall c r ⊆ s → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
intro c r rp cs
Proof 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 : ℕ → ℂ → ℝ
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
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
have sm := fun n ↦ ((fs n).mono cs).submean rp
Proof 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 : ℕ → ℂ → ℝ
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)
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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)
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
have r0 : 0 ≤ r := rp.le
Proof 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 : ℕ → ℂ → ℝ
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
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
have cts : ∀ t, circleMap c r t ∈ s := fun _ ↦ cs (circleMap_mem_closedBall _ r0 _)
Proof 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 : ℕ → ℂ → ℝ
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
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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
mt : Tendsto (fun n => ⨍ (t : ℝ) in itau, f n (circleMap c r t)) atTop (𝓝 (⨍ (t : ℝ) in itau, g (circleMap c r t)))
⊢ g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
exact le_of_tendsto_of_tendsto' (ft c (cs (Metric.mem_closedBall_self r0))) mt sm
Proof state after:
no goals
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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
⊢ Tendsto (fun n => ⨍ (t : ℝ) in itau, f n (circleMap c r t)) atTop (𝓝 (⨍ (t : ℝ) in itau, g (circleMap c r t)))
Tactic:
simp_rw [average_eq]
Proof 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 : ℕ → ℂ → ℝ
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
⊢ Tendsto (fun n => (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, f n (circleMap c r t)) atTop
    (𝓝 ((↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, g (circleMap c r t)))
Theorem: SubharmonicOn.monotone_lim
Proof 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 : ℕ → ℂ → ℝ
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
⊢ Tendsto (fun n => (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, f n (circleMap c r t)) atTop
    (𝓝 ((↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, g (circleMap c r t)))
Tactic:
apply Filter.Tendsto.const_smul
Proof state after:
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
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
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
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
Tactic:
set b' := fun z ↦ |f 0 z| + |g z|
Proof state after:
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|
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
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|
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
Tactic:
set b := fun t ↦ b' (circleMap c r t)
Proof state after:
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)
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
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)
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
Tactic:
have bc' : ContinuousOn b' (closedBall c r) :=
  ContinuousOn.add ((fs 0).mono cs).cont.abs (gc.mono cs).abs
Proof state after:
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)
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))