internlm/Lean-Github huggingface dataset:
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ r2 * (d.toReal / e.toReal).sqrt > 0
Tactic:
exact mul_pos r2p (Real.sqrt_pos_of_pos (div_pos drp erp))
Proof state after:
no goals
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ r1 < r2
Tactic:
rw [← hr1]
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 : ℕ → ℂ → ℝ≥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
⊢ r2 * (d.toReal / e.toReal).sqrt < r2
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ r2 * (d.toReal / e.toReal).sqrt < r2
Tactic:
apply mul_lt_of_lt_one_right r2p
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 : ℕ → ℂ → ℝ≥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
⊢ (d.toReal / e.toReal).sqrt < 1
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ (d.toReal / e.toReal).sqrt < 1
Tactic:
rw [Real.sqrt_lt dep.le zero_le_one]
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 : ℕ → ℂ → ℝ≥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
⊢ d.toReal / e.toReal < 1 ^ 2
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ d.toReal / e.toReal < 1 ^ 2
Tactic:
simp only [one_pow]
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 : ℕ → ℂ → ℝ≥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
⊢ d.toReal / e.toReal < 1
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ d.toReal / e.toReal < 1
Tactic:
apply (div_lt_one erp).mpr
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 : ℕ → ℂ → ℝ≥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
⊢ d.toReal < e.toReal
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ d.toReal < e.toReal
Tactic:
exact (ENNReal.toReal_lt_toReal df ef).mpr de
Proof state after:
no goals
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
⊢ r1 < r
Tactic:
apply _root_.trans r12
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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
⊢ r2 < r
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
⊢ r2 < r
Tactic:
rw [← hr2]
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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
⊢ r / 2 < r
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
⊢ r / 2 < r
Tactic:
exact half_lt_self rp
Proof state after:
no goals
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
⊢ d = e * (ENNReal.ofReal (π * r1 ^ 2) * ENNReal.ofReal (π * r2 ^ 2)⁻¹)
Tactic:
rw [← ENNReal.ofReal_mul (by bound : π * r1 ^ 2 ≥ 0), ← hr1, mul_pow, Real.sq_sqrt dep.le]
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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
⊢ d = e * ENNReal.ofReal (π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹)
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
⊢ d = e * ENNReal.ofReal (π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹)
Tactic:
have smash : π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹ = d.toReal / e.toReal := by
  calc π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹
    _ = π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π⁻¹ * (r2 ^ 2)⁻¹) := by simp_rw [mul_inv]
    _ = d.toReal / e.toReal * (π * π⁻¹) * (r2 ^ 2 * (r2 ^ 2)⁻¹) := by ring_nf
    _ = d.toReal / e.toReal := by simp only [mul_inv_cancel Real.pi_pos.ne',
        mul_inv_cancel (pow_ne_zero _ r2p.ne'), mul_one]
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 : ℕ → ℂ → ℝ≥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
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
smash : π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹ = d.toReal / e.toReal
⊢ d = e * ENNReal.ofReal (π * (r2 ^ 2 * (d.toReal / e.toReal)) * (π * r2 ^ 2)⁻¹)