Theorem: AnalyticOn.maxLog_norm_subharmonicOn (Ray/Hartogs/Subharmonic.lean)

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
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

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)
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

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
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

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
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

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
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

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
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

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
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

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]
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

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
State after:
no goals

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
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

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]
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

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 : ℂ
⊢ (partialSups fun k => maxLog b✝ (Complex.abs ((duals k) (f z)))) a ≤
    (partialSups fun k => maxLog b✝ (Complex.abs ((duals k) (f z)))) b
Tactic:
apply (partialSups _).monotone ab
State after:
no goals