internlm/Lean-Github huggingface dataset:
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 ((fun n z => ENNReal.ofReal (-f' n z)) n) (interior s)
Tactic:
exact fun n ↦ ((fs' n).mono interior_subset).neg (fn' n) measurableSet_interior
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
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
⊢ ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
Tactic:
intro z zs
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
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
z : ℂ
zs : z ∈ interior s
⊢ liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
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
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
z : ℂ
zs : z ∈ interior s
⊢ liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
Tactic:
specialize fc z (interior_subset zs)
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
⊢ liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
⊢ liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
Tactic:
refine le_liminf.simple.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 : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
⊢ ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
⊢ ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
Tactic:
intro d dc
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
Tactic:
have df : d ≠ ⊤ := ne_top_of_lt dc
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
Tactic:
have dc' : b - d.toReal > c := by
  calc b - d.toReal
    _ > b - (ENNReal.ofReal (b - c)).toReal :=
      sub_lt_sub_left ((ENNReal.toReal_lt_toReal df ENNReal.ofReal_ne_top).mpr dc) b
    _ = b - (b - c) := by rw [ENNReal.toReal_ofReal (sub_pos.mpr bc).le]
    _ = c := by ring_nf
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ g n z
Tactic:
refine (fc _ dc').mp (Filter.eventually_of_forall ?_)
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
⊢ ∀ (x : ℕ), f x z ≤ b - d.toReal → d ≤ g x z
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
⊢ ∀ (x : ℕ), f x z ≤ b - d.toReal → d ≤ g x z
Tactic:
intro n fb
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
n : ℕ
fb : f n z ≤ b - d.toReal
⊢ d ≤ g n z
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
n : ℕ
fb : f n z ≤ b - d.toReal
⊢ d ≤ g n z
Tactic:
calc
  g n z = ENNReal.ofReal (b - f n z) := by simp only [← hg, ← hf', neg_sub]
  _ ≥ ENNReal.ofReal (b - (b - d.toReal)) := by bound
  _ = ENNReal.ofReal d.toReal := by ring_nf
  _ = d := by rw [ENNReal.ofReal_toReal df]
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
⊢ b - d.toReal > c
Tactic:
calc b - d.toReal
  _ > b - (ENNReal.ofReal (b - c)).toReal :=
    sub_lt_sub_left ((ENNReal.toReal_lt_toReal df ENNReal.ofReal_ne_top).mpr dc) b
  _ = b - (b - c) := by rw [ENNReal.toReal_ofReal (sub_pos.mpr bc).le]
  _ = c := by ring_nf
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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
⊢ b - (ENNReal.ofReal (b - c)).toReal = b - (b - c)
Tactic:
rw [ENNReal.toReal_ofReal (sub_pos.mpr bc).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
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)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
⊢ b - (b - c) = c
Tactic:
ring_nf
Proof state after:
no goals