Theorem: SuperharmonicOn.hartogs
Proof state before:
case neg.intro.intro.hnhds.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
r2p : r2 > 0
r1p : r1 > 0
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
rde : d = e * (ENNReal.ofReal (π * r1 ^ 2) * ENNReal.ofReal (π * r2 ^ 2)⁻¹)
s12 : ∀ w ∈ closedBall z (r2 - r1), closedBall z r1 ⊆ closedBall w r2
r2s : ∀ w ∈ closedBall z (r2 - r1), closedBall w r2 ⊆ s
fi : ℂ → ℝ≥0∞ := fun z => liminf (fun n => f n z) atTop
fm : ∀ (n : ℕ), _root_.AEMeasurable (f n) (volume.restrict (closedBall z r1))
fatou' :
  ∫⁻ (a : ℂ) in closedBall z r1, liminf (fun n => f n a) atTop ≤
    liminf (fun n => ∫⁻ (a : ℂ) in closedBall z r1, f n a) atTop
im : c * ↑volume (closedBall z r1) ≤ ∫⁻ (x : ℂ) in closedBall z r1, liminf (fun n => f n x) atTop
vec : e * ↑volume (closedBall z r1) < c * ↑volume (closedBall z r1)
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d
Tactic:
have fatou := le_liminf.simple.mp (_root_.trans im fatou') (e * volume (closedBall z r1)) vec
Proof state after:
case neg.intro.intro.hnhds.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
dz : ¬d = 0
dp : d > 0
df : d ≠ ⊤
drp : d.toReal > 0
e : ℝ≥0∞
de : d < e
ec : e < c
ep : e > 0
ez : e ≠ 0
ef : e ≠ ⊤
erp : e.toReal > 0
z : ℂ
zs : z ∈ k
r : ℝ
rp : r > 0
rs : ball z r ⊆ interior s
r2 : ℝ
hr2 : r / 2 = r2
r1 : ℝ
hr1 : r2 * (d.toReal / e.toReal).sqrt = r1
dep : d.toReal / e.toReal > 0
r2p : r2 > 0
r1p : r1 > 0
r12 : r1 < r2
r1r : r1 < r
r1s : closedBall z r1 ⊆ s
rde : d = e * (ENNReal.ofReal (π * r1 ^ 2) * ENNReal.ofReal (π * r2 ^ 2)⁻¹)
s12 : ∀ w ∈ closedBall z (r2 - r1), closedBall z r1 ⊆ closedBall w r2
r2s : ∀ w ∈ closedBall z (r2 - r1), closedBall w r2 ⊆ s
fi : ℂ → ℝ≥0∞ := fun z => liminf (fun n => f n z) atTop
fm : ∀ (n : ℕ), _root_.AEMeasurable (f n) (volume.restrict (closedBall z r1))
fatou' :
  ∫⁻ (a : ℂ) in closedBall z r1, liminf (fun n => f n a) atTop ≤
    liminf (fun n => ∫⁻ (a : ℂ) in closedBall z r1, f n a) atTop
im : c * ↑volume (closedBall z r1) ≤ ∫⁻ (x : ℂ) in closedBall z r1, liminf (fun n => f n x) atTop
vec : e * ↑volume (closedBall z r1) < c * ↑volume (closedBall z r1)
fatou : ∀ᶠ (n : ℕ) in atTop, e * ↑volume (closedBall z r1) ≤ ∫⁻ (a : ℂ) in closedBall z r1, f n a
⊢ ∃ t ∈ 𝓝[k] z, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ t, f n z ≥ d