internlm/Lean-Github huggingface dataset:
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
have ep : e > 0 := _root_.trans de dp
Proof state after:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
have ez : e ≠ 0 := pos_iff_ne_zero.mp ep
Proof state after:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
have ef : e ≠ ⊤ := ne_top_of_lt ec
Proof state after:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
have erp : e.toReal > 0 := ENNReal.toReal_pos ez ef
Proof state after:
case neg.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
intro z zs
Proof state after:
case neg.intro.intro.hnhds
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior z (ks zs) with ⟨r, rp, rs⟩
Proof state after:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
generalize hr2 : r / 2 = r2
Proof state after:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
generalize hr1 : r2 * Real.sqrt (d.toReal / e.toReal) = r1
Proof state after:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
have dep : d.toReal / e.toReal > 0 := div_pos drp erp
Proof state after:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
have r2p : r2 > 0 := by rw [← hr2]; exact half_pos rp
Proof state after:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
r2p : r2 > 0
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
r2p : r2 > 0
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
have r1p : r1 > 0 := by rw [← hr1]; exact mul_pos r2p (Real.sqrt_pos_of_pos (div_pos drp erp))
Proof state after:
case neg.intro.intro.hnhds.intro.intro
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 : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
r2p : r2 > 0
r1p : r1 > 0
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d