internlm/Lean-Github huggingface dataset:
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)
⊢ Tendsto (fun x => ∫ (t : ℝ) in itau, f x (circleMap c r t)) atTop (𝓝 (∫ (t : ℝ) in itau, g (circleMap c r t)))
Tactic:
have fcc : ∀ n, Continuous fun t ↦ f n (circleMap c r t) := fun n ↦
  ((fs n).cont.mono cs).comp_continuous (continuous_circleMap _ _) fun t ↦
    circleMap_mem_closedBall _ r0 _
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)
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)))
Theorem: SubharmonicOn.monotone_lim
Proof state before:
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)
Tactic:
intro n
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)
Theorem: SubharmonicOn.monotone_lim
Proof state before:
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)
Tactic:
exact (fcc n).aestronglyMeasurable
Proof state after:
no goals
Theorem: SubharmonicOn.monotone_lim
Proof state before:
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)
Tactic:
exact bc'.integrableOn_sphere rp
Proof state after:
no goals
Theorem: SubharmonicOn.monotone_lim
Proof state before:
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
Tactic:
intro n
Proof state after:
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
Theorem: SubharmonicOn.monotone_lim
Proof state before:
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
Tactic:
rw [ae_restrict_iff' measurableSet_itau]
Proof state after:
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 : ℕ
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ itau → ‖f n (circleMap c r x)‖ ≤ b x
Theorem: SubharmonicOn.monotone_lim
Proof state before:
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 : ℕ
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ itau → ‖f n (circleMap c r x)‖ ≤ b x
Tactic:
apply ae_of_all
Proof state after:
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 : ℕ
⊢ ∀ a ∈ itau, ‖f n (circleMap c r a)‖ ≤ b a
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 : ℕ
⊢ ∀ a ∈ itau, ‖f n (circleMap c r a)‖ ≤ b a
Tactic:
intro t _
Proof state after:
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
⊢ ‖f n (circleMap c r t)‖ ≤ b t
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
⊢ ‖f n (circleMap c r t)‖ ≤ b t
Tactic:
generalize hz : circleMap c r t = z
Proof state after:
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
⊢ ‖f n z‖ ≤ b t
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
⊢ ‖f n z‖ ≤ b t
Tactic:
have zs : z ∈ s := by rw [← hz]; apply cts
Proof state after:
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
⊢ ‖f n z‖ ≤ b t
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
⊢ ‖f n z‖ ≤ b t
Tactic:
rw [Real.norm_eq_abs]
Proof state after:
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
⊢ |f n z| ≤ b t