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 : ¬b ≤ c
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
simp only [not_le] at bc
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
⊢ ∀ d > 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
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
generalize hf' : (fun n z ↦ f n z - b) = f'
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'
⊢ ∀ d > 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'
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
generalize hg : (fun n z ↦ ENNReal.ofReal (-f' n z)) = g
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
⊢ ∀ d > 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
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have fs' : ∀ n, SubharmonicOn (f' n) s := by
  rw [← hf']; exact fun n ↦ (fs n).add (HarmonicOn.const _).subharmonicOn
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
⊢ ∀ d > 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
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have fn' : ∀ n z, z ∈ interior s → f' n z ≤ 0 := fun n z zs ↦ by
  simp only [← hf', fb n z (interior_subset zs), sub_nonpos]
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
⊢ ∀ d > 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
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have gs : ∀ n, SuperharmonicOn (g n) (interior s) := by
  rw [← hg]; exact fun n ↦ ((fs' n).mono interior_subset).neg (fn' n) measurableSet_interior
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)
⊢ ∀ d > 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)
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have gc : ∀ z, z ∈ interior s → (atTop.liminf fun n ↦ g n z) ≥ ENNReal.ofReal (b - c) := by
  intro z zs; specialize fc z (interior_subset zs); refine le_liminf.simple.mpr ?_
  intro d dc
  have df : d ≠ ⊤ := ne_top_of_lt dc
  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
  refine (fc _ dc').mp (Filter.eventually_of_forall ?_); intro n fb
  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:
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)
⊢ ∀ d > 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)
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have ks' := ks
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 s
⊢ ∀ d > 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 s
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
rw [← interior_interior] at ks'
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)
⊢ ∀ d > 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)
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have h := SuperharmonicOn.hartogs gs gc ck ks'
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 > 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 > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
intro d dc
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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d