internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.neg
Proof state before:
case h.a
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ f c ≤ ⨍ (x : ℂ) in closedBall c r, f x

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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ 0 ≤ (π * r ^ 2)⁻¹
Tactic:
exact (fs.mono cs).submean_disk rp
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ 0 ≤ (π * r ^ 2)⁻¹
Theorem: SubharmonicOn.neg
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ 0 ≤ (π * r ^ 2)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.neg
Proof state before:
case hfi
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ Integrable (fun z => -f z) (volume.restrict (closedBall c r))
Tactic:
exact (fs.mono cs).cont.neg.integrableOn_closedBall
Proof state after:
no goals
Theorem: SubharmonicOn.neg
Proof state before:
case f_nn
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (volume.restrict (closedBall c r)).ae.EventuallyLE 0 fun z => -f z
Tactic:
rw [Filter.EventuallyLE]
Proof state after:
case f_nn
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ∀ᵐ (x : ℂ) ∂volume.restrict (closedBall c r), 0 x ≤ -f x
Theorem: SubharmonicOn.neg
Proof state before:
case f_nn
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ∀ᵐ (x : ℂ) ∂volume.restrict (closedBall c r), 0 x ≤ -f x
Tactic:
rw [ae_restrict_iff' measurableSet_closedBall]
Proof state after:
case f_nn
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ∀ᵐ (x : ℂ), x ∈ closedBall c r → 0 x ≤ -f x
Theorem: SubharmonicOn.neg
Proof state before:
case f_nn
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ∀ᵐ (x : ℂ), x ∈ closedBall c r → 0 x ≤ -f x
Tactic:
apply Filter.eventually_of_forall
Proof state after:
case f_nn.hp
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ∀ x ∈ closedBall c r, 0 x ≤ -f x
Theorem: SubharmonicOn.neg
Proof state before:
case f_nn.hp
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ∀ x ∈ closedBall c r, 0 x ≤ -f x
Tactic:
intro z zs
Proof state after:
case f_nn.hp
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
z : ℂ
zs : z ∈ closedBall c r
⊢ 0 z ≤ -f z
Theorem: SubharmonicOn.neg
Proof state before:
case f_nn.hp
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
z : ℂ
zs : z ∈ closedBall c r
⊢ 0 z ≤ -f z
Tactic:
simp only [Pi.zero_apply, Right.nonneg_neg_iff]
Proof state after:
case f_nn.hp
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
z : ℂ
zs : z ∈ closedBall c r
⊢ f z ≤ 0
Theorem: SubharmonicOn.neg
Proof state before:
case f_nn.hp
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 : Set ℂ
fs : SubharmonicOn f s
fn : ∀ z ∈ s, f z ≤ 0
sm : MeasurableSet s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
z : ℂ
zs : z ∈ closedBall c r
⊢ f z ≤ 0
Tactic:
exact fn z (cs zs)
Proof state after:
no goals
Theorem: NNReal.pi_eq_ofReal_pi
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
⊢ ↑pi = ENNReal.ofReal π
Tactic:
rw [←NNReal.coe_real_pi, ENNReal.ofReal_coe_nnreal]
Proof state after:
no goals
Theorem: SuperharmonicOn.hartogs
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
⊢ ∀ d < c, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
intro d dc
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.hartogs
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℕ → ℂ → ℝ≥0∞
s k : Set ℂ
c : ℝ≥0∞
fs : ∀ (n : ℕ), SuperharmonicOn (f n) s
fc : ∀ z ∈ s, liminf (fun n => f n z) atTop ≥ c
ck : IsCompact k
ks : k ⊆ interior s
d : ℝ≥0∞
dc : d < c
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
by_cases dz : d = 0
Proof 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 : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (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 : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
have dp : d > 0 := pos_iff_ne_zero.mpr dz
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 : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
have df : d ≠ ⊤ := ne_top_of_lt 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 : ℕ → ℂ → ℝ≥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 ≠ ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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 ≠ ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
have drp : d.toReal > 0 := ENNReal.toReal_pos dz 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 : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Theorem: SuperharmonicOn.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 : ℕ → ℂ → ℝ≥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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d
Tactic:
rcases exists_between dc with ⟨e, de, ec⟩
Proof state after:
case neg.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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, f n z ≥ d