internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.hartogs
Proof state before:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c) := by
  rw [ENNReal.ofReal_lt_ofReal_iff (sub_pos.mpr bc)]; simpa only [sub_lt_sub_iff_left]
Proof state after:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Theorem: SubharmonicOn.hartogs
Proof state before:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
refine (h _ dc').mp (Filter.eventually_of_forall ?_)
Proof state after:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ (x : ℕ), (∀ z ∈ k, g x z ≥ ENNReal.ofReal (b - d)) → ∀ z ∈ k, f x z ≤ d
Theorem: SubharmonicOn.hartogs
Proof state before:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ (x : ℕ), (∀ z ∈ k, g x z ≥ ENNReal.ofReal (b - d)) → ∀ z ∈ k, f x z ≤ d
Tactic:
intro n hn z zk
Proof state after:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
hn : ∀ z ∈ k, g n z ≥ ENNReal.ofReal (b - d)
z : ℂ
zk : z ∈ k
⊢ f n z ≤ d
Theorem: SubharmonicOn.hartogs
Proof state before:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
hn : ∀ z ∈ k, g n z ≥ ENNReal.ofReal (b - d)
z : ℂ
zk : z ∈ k
⊢ f n z ≤ d
Tactic:
specialize hn z zk
Proof state after:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : g n z ≥ ENNReal.ofReal (b - d)
⊢ f n z ≤ d
Theorem: SubharmonicOn.hartogs
Proof state before:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : g n z ≥ ENNReal.ofReal (b - d)
⊢ f n z ≤ d
Tactic:
simp only [← hg, ← hf', neg_sub, ge_iff_le] at hn
Proof state after:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : ENNReal.ofReal (b - d) ≤ ENNReal.ofReal (b - f n z)
⊢ f n z ≤ d
Theorem: SubharmonicOn.hartogs
Proof state before:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : ENNReal.ofReal (b - d) ≤ ENNReal.ofReal (b - f n z)
⊢ f n z ≤ d
Tactic:
rw [ENNReal.ofReal_le_ofReal_iff (sub_nonneg.mpr (fb n z (interior_subset (ks zk))))] at hn
Proof state after:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : b - d ≤ b - f n z
⊢ f n z ≤ d
Theorem: SubharmonicOn.hartogs
Proof state before:
case neg
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : b - d ≤ b - f n z
⊢ f n z ≤ d
Tactic:
rwa [← sub_le_sub_iff_left]
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
Proof state before:
case pos
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : b ≤ c
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
exact fun d dc ↦
  Filter.eventually_of_forall fun n z zk ↦
    _root_.trans (fb n z (_root_.trans ks interior_subset zk)) (_root_.trans bc dc.le)
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
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 : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
⊢ ∀ (n : ℕ), SubharmonicOn (f' n) s
Tactic:
rw [← hf']
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 : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
⊢ ∀ (n : ℕ), SubharmonicOn ((fun n z => f n z - b) n) s
Theorem: SubharmonicOn.hartogs
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 : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
⊢ ∀ (n : ℕ), SubharmonicOn ((fun n z => f n z - b) n) s
Tactic:
exact fun n ↦ (fs n).add (HarmonicOn.const _).subharmonicOn
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
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 : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
n : ℕ
z : ℂ
zs : z ∈ interior s
⊢ f' n z ≤ 0
Tactic:
simp only [← hf', fb n z (interior_subset zs), sub_nonpos]
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
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 : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
⊢ ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
Tactic:
rw [← hg]
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 : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
⊢ ∀ (n : ℕ), SuperharmonicOn ((fun n z => ENNReal.ofReal (-f' n z)) n) (interior s)