internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
⊢ IsMaxOn f s w
Tactic:
generalize hr : abs (w - x) = r
Proof state after:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
⊢ IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case intro.intro.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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
⊢ IsMaxOn f s w
Tactic:
by_cases wx : w = x
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : w = x
⊢ IsMaxOn f s w

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 : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ IsMaxOn f s w
Tactic:
have rp : r > 0 := by
  simp only [← hr, AbsoluteValue.pos_iff, Ne]; exact sub_ne_zero.mpr wx
Proof state after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w
Tactic:
rw [dist_comm, Complex.dist_eq, hr] at h
Proof state after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ IsMaxOn f s w
Tactic:
have rs : closedBall x r ⊆ s := by
  rw [← closure_ball x rp.ne', ← sc.isClosed.closure_eq]; apply closure_mono
  rw [← h]; apply Metric.ball_infDist_compl_subset
Proof state after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
⊢ IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
⊢ IsMaxOn f s w
Tactic:
have rm : IsMaxOn f (closedBall x r) x := by intro y ys; exact xm (rs ys)
Proof state after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ IsMaxOn f s w
Tactic:
have wx : f x = f w := by
  apply SubharmonicOn.maximum_principle_ball (fs.mono rs) rp rm
  simp only [Complex.dist_eq, Metric.mem_closedBall, hr, le_refl]
Proof state after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
⊢ IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
⊢ IsMaxOn f s w
Tactic:
intro y ys
Proof state after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x | (fun x => f x ≤ f w) x}
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x | (fun x => f x ≤ f w) x}
Tactic:
rw [← wx]
Proof state after:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case neg
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx✝ : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
wx : f x = f w
y : ℂ
ys : y ∈ s
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}
Tactic:
exact xm ys
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle
Proof 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 : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : w = x
⊢ IsMaxOn f s w
Tactic:
rwa [wx]
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle
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
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ r > 0
Tactic:
simp only [← hr, AbsoluteValue.pos_iff, Ne]
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
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ ¬w - x = 0
Theorem: SubharmonicOn.maximum_principle
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
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
h : Metric.infDist x sᶜ = dist x w
r : ℝ
hr : Complex.abs (w - x) = r
wx : ¬w = x
⊢ ¬w - x = 0
Tactic:
exact sub_ne_zero.mpr wx
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle
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
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ closedBall x r ⊆ s
Tactic:
rw [← closure_ball x rp.ne', ← sc.isClosed.closure_eq]
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
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ closure (ball x r) ⊆ closure s
Theorem: SubharmonicOn.maximum_principle
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
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ closure (ball x r) ⊆ closure s
Tactic:
apply closure_mono
Proof state after:
case h
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
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x r ⊆ s