Theorem: SubharmonicOn.hartogs (Ray/Hartogs/Subharmonic.lean)

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
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
by_cases bc : b ≤ c
State after:
case pos
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : b ≤ c
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d

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

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
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

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'
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

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
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

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
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

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]
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

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
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

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]
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

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
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

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'
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

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'
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

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
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

State before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
have dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c) := by
  rw [ENNReal.ofReal_lt_ofReal_iff (sub_pos.mpr bc)]; simpa only [sub_lt_sub_iff_left]
State after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d

State before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
refine (h _ dc').mp (Filter.eventually_of_forall ?_)
State after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ (x : ℕ), (∀ z ∈ k, g x z ≥ ENNReal.ofReal (b - d)) → ∀ z ∈ k, f x z ≤ d

State before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
⊢ ∀ (x : ℕ), (∀ z ∈ k, g x z ≥ ENNReal.ofReal (b - d)) → ∀ z ∈ k, f x z ≤ d
Tactic:
intro n hn z zk
State after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
hn : ∀ z ∈ k, g n z ≥ ENNReal.ofReal (b - d)
z : ℂ
zk : z ∈ k
⊢ f n z ≤ d

State before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
hn : ∀ z ∈ k, g n z ≥ ENNReal.ofReal (b - d)
z : ℂ
zk : z ∈ k
⊢ f n z ≤ d
Tactic:
specialize hn z zk
State after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : g n z ≥ ENNReal.ofReal (b - d)
⊢ f n z ≤ d

State before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : g n z ≥ ENNReal.ofReal (b - d)
⊢ f n z ≤ d
Tactic:
simp only [← hg, ← hf', neg_sub, ge_iff_le] at hn
State after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : ENNReal.ofReal (b - d) ≤ ENNReal.ofReal (b - f n z)
⊢ f n z ≤ d

State before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : ENNReal.ofReal (b - d) ≤ ENNReal.ofReal (b - f n z)
⊢ f n z ≤ d
Tactic:
rw [ENNReal.ofReal_le_ofReal_iff (sub_nonneg.mpr (fb n z (interior_subset (ks zk))))] at hn
State after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : b - d ≤ b - f n z
⊢ f n z ≤ d

State before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
dc' : ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
n : ℕ
z : ℂ
zk : z ∈ k
hn : b - d ≤ b - f n z
⊢ f n z ≤ d
Tactic:
rwa [← sub_le_sub_iff_left]
State after:
no goals

State before:
case pos
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : b ≤ c
⊢ ∀ d > c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≤ d
Tactic:
exact fun d dc ↦
  Filter.eventually_of_forall fun n z zk ↦
    _root_.trans (fb n z (_root_.trans ks interior_subset zk)) (_root_.trans bc dc.le)
State after:
no goals

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
⊢ ∀ (n : ℕ), SubharmonicOn (f' n) s
Tactic:
rw [← hf']
State after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
⊢ ∀ (n : ℕ), SubharmonicOn ((fun n z => f n z - b) n) s

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
⊢ ∀ (n : ℕ), SubharmonicOn ((fun n z => f n z - b) n) s
Tactic:
exact fun n ↦ (fs n).add (HarmonicOn.const _).subharmonicOn
State after:
no goals

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
n : ℕ
z : ℂ
zs : z ∈ interior s
⊢ f' n z ≤ 0
Tactic:
simp only [← hf', fb n z (interior_subset zs), sub_nonpos]
State after:
no goals

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
⊢ ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
Tactic:
rw [← hg]
State after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ
s k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
⊢ ∀ (n : ℕ), SuperharmonicOn ((fun n z => ENNReal.ofReal (-f' n z)) n) (interior s)

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
State after:
no goals

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
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)

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)
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)

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 ?_
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

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
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

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
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

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
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

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 ?_)
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

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
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

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
⊢ g n z = ENNReal.ofReal (b - f n z)
Tactic:
simp only [← hg, ← hf', neg_sub]
State after:
no goals

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
⊢ ENNReal.ofReal (b - f n z) ≥ ENNReal.ofReal (b - (b - d.toReal))
Tactic:
bound
State after:
no goals

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
⊢ ENNReal.ofReal (b - (b - d.toReal)) = ENNReal.ofReal d.toReal
Tactic:
ring_nf
State after:
no goals

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
⊢ ENNReal.ofReal d.toReal = d
Tactic:
rw [ENNReal.ofReal_toReal df]
State after:
no goals

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)
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
⊢ ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
Tactic:
rw [ENNReal.ofReal_lt_ofReal_iff (sub_pos.mpr bc)]
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)
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
⊢ b - d < b - c

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)
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
⊢ b - d < b - c
Tactic:
simpa only [sub_lt_sub_iff_left]
State after:
no goals