internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.monotone_lim
Proof state before:
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)
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ itau → Tendsto (fun n => f n (circleMap c r x)) atTop (𝓝 (g (circleMap c r x)))
Tactic:
apply ae_of_all
Proof state after:
case hf.h_lim.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)
⊢ ∀ a ∈ itau, Tendsto (fun n => f n (circleMap c r a)) atTop (𝓝 (g (circleMap c r a)))
Theorem: SubharmonicOn.monotone_lim
Proof state before:
case hf.h_lim.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)
⊢ ∀ a ∈ itau, Tendsto (fun n => f n (circleMap c r a)) atTop (𝓝 (g (circleMap c r a)))
Tactic:
intro t _
Proof state after:
case hf.h_lim.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)
t : ℝ
a✝ : t ∈ itau
⊢ Tendsto (fun n => f n (circleMap c r t)) atTop (𝓝 (g (circleMap c r t)))
Theorem: SubharmonicOn.monotone_lim
Proof state before:
case hf.h_lim.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)
t : ℝ
a✝ : t ∈ itau
⊢ Tendsto (fun n => f n (circleMap c r t)) atTop (𝓝 (g (circleMap c r t)))
Tactic:
exact ft _ (cts _)
Proof state after:
no goals
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
⊢ SubharmonicOn (fun z => maxLog b ‖f z‖) s
Tactic:
have gc := fa.continuousOn.maxLog_norm b
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
⊢ SubharmonicOn (fun z => maxLog b ‖f z‖) s
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
⊢ SubharmonicOn (fun z => maxLog b ‖f z‖) s
Tactic:
have ft := fun z (_ : z ∈ s) ↦ duals_lim_tendsto_maxLog_norm b (f z)
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
⊢ SubharmonicOn (fun z => maxLog b ‖f z‖) s
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
⊢ SubharmonicOn (fun z => maxLog b ‖f z‖) s
Tactic:
have fs : ∀ n, SubharmonicOn (fun z ↦ partialSups (fun k ↦ maxLog b ‖duals k (f z)‖) n) s := by
  intro m; apply SubharmonicOn.partialSups; intro n; simp_rw [Complex.norm_eq_abs]
  exact ((duals n).comp_analyticOn fa).maxLogAbsSubharmonicOn b
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) n) s
⊢ SubharmonicOn (fun z => maxLog b ‖f z‖) s
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) n) s
⊢ SubharmonicOn (fun z => maxLog b ‖f z‖) s
Tactic:
refine SubharmonicOn.monotone_lim fs ?_ ft 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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) n) s
⊢ Monotone fun n z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) n
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
⊢ ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) n) s
Tactic:
intro m
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m : ℕ
⊢ SubharmonicOn (fun z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) m) s
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m : ℕ
⊢ SubharmonicOn (fun z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) m) s
Tactic:
apply SubharmonicOn.partialSups
Proof state after:
case fs
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m : ℕ
⊢ ∀ (n : ℕ), SubharmonicOn (fun z => maxLog b ‖(duals n) (f z)‖) s
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
Proof state before:
case fs
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m : ℕ
⊢ ∀ (n : ℕ), SubharmonicOn (fun z => maxLog b ‖(duals n) (f z)‖) s
Tactic:
intro n
Proof state after:
case fs
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m n : ℕ
⊢ SubharmonicOn (fun z => maxLog b ‖(duals n) (f z)‖) s
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
Proof state before:
case fs
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m n : ℕ
⊢ SubharmonicOn (fun z => maxLog b ‖(duals n) (f z)‖) s
Tactic:
simp_rw [Complex.norm_eq_abs]
Proof state after:
case fs
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m n : ℕ
⊢ SubharmonicOn (fun z => maxLog b (Complex.abs ((duals n) (f z)))) s
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
Proof state before:
case fs
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
m n : ℕ
⊢ SubharmonicOn (fun z => maxLog b (Complex.abs ((duals n) (f z)))) s
Tactic:
exact ((duals n).comp_analyticOn fa).maxLogAbsSubharmonicOn b
Proof state after:
no goals
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
gc : ContinuousOn (fun z => maxLog b ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) n) s
⊢ Monotone fun n z => (partialSups fun k => maxLog b ‖(duals k) (f z)‖) n
Tactic:
intro a b ab z
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b✝ : ℝ
gc : ContinuousOn (fun z => maxLog b✝ ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b✝ ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) s
a b : ℕ
ab : a ≤ b
z : ℂ
⊢ (fun n z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) a z ≤
    (fun n z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) b z
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b✝ : ℝ
gc : ContinuousOn (fun z => maxLog b✝ ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b✝ ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) s
a b : ℕ
ab : a ≤ b
z : ℂ
⊢ (fun n z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) a z ≤
    (fun n z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) b z
Tactic:
simp only [Complex.norm_eq_abs]
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 : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b✝ : ℝ
gc : ContinuousOn (fun z => maxLog b✝ ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b✝ ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) s
a b : ℕ
ab : a ≤ b
z : ℂ
⊢ (partialSups fun k => maxLog b✝ (Complex.abs ((duals k) (f z)))) a ≤
    (partialSups fun k => maxLog b✝ (Complex.abs ((duals k) (f z)))) b