internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ e' + t ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
⊢ ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
Tactic:
intro x _
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ f (circleMap z e' x) ≤ f c
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ f (circleMap z e' x) ≤ f c
Tactic:
apply isMaxOn_iff.mp cm
Proof state after:
case 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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall c r
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
case 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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall c r
Tactic:
apply ss
Proof state after:
case a.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall z e'
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
case a.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
x : ℝ
a✝ : x ∈ itau
⊢ circleMap z e' x ∈ closedBall z e'
Tactic:
simp only [Complex.dist_eq, Metric.mem_closedBall, circleMap_sub_center, abs_circleMap_zero,
  abs_of_pos e'p, le_refl]
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ ContinuousOn (fun a => f (circleMap z e' a)) itau
Tactic:
apply (fs.cont.mono ss).comp (continuous_circleMap _ _).continuousOn
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ Set.MapsTo (circleMap z e') itau (closedBall z e')
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
⊢ Set.MapsTo (circleMap z e') itau (closedBall z e')
Tactic:
intro a _
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
a : ℝ
a✝ : a ∈ itau
⊢ circleMap z e' a ∈ closedBall z e'
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
a : ℝ
a✝ : a ∈ itau
⊢ circleMap z e' a ∈ closedBall z e'
Tactic:
simp only [Complex.dist_eq, abs_of_pos e'p, Metric.mem_closedBall, circleMap_sub_center,
  abs_circleMap_zero, le_refl]
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
t : ℝ
z : ℂ
hz : c + ↑t * y = z
fz : f (c + ↑t * y) = f c
tp : 0 ≤ t
tu : t < u
tz : Complex.abs (z - c) = t
zs : z ∈ interior (closedBall c r)
e : ℝ
ep : 0 < e
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
teu : t + e' ≤ u
e's : e' < e
lo : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
ss : closedBall z e' ⊆ closedBall c r
hi : ∀ x ∈ itau, f (circleMap z e' x) ≤ f c
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
fw : ∀ x ∈ itau, f (circleMap z e' x) = f c
⊢ z + ↑e' * y ∈ sphere z e'
Tactic:
simp only [abs_of_pos e'p, y1, mem_sphere_iff_norm, add_sub_cancel_left,
  Complex.norm_eq_abs, AbsoluteValue.map_mul, Complex.abs_ofReal, mul_one]
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
u : ℝ
hu : Complex.abs (g - c) = u
u0 : u > 0
ur : u ≤ r
y : ℂ
hy : (g - c) / ↑u = y
y1 : Complex.abs y = 1
s : Set ℝ
hs : (fun t => f (c + ↑t * y)) ⁻¹' {f c} = s
s0 : 0 ∈ s
us : f (c + ↑u * ((g - c) / ↑u)) = f c
⊢ ↑u ≠ 0
Tactic:
simp only [u0.ne', Ne, Complex.ofReal_eq_zero, not_false_iff]
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
⊢ ∃ w ∈ frontier s, IsMaxOn f s w
Tactic:
rcases sc.exists_isMaxOn sn fs.cont with ⟨x, xs, xm⟩
Proof state after:
case 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 ∈ frontier s, IsMaxOn f s w
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case 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 ∈ frontier s, IsMaxOn f s w
Tactic:
rcases exists_mem_frontier_infDist_compl_eq_dist xs sc.ne_univ with ⟨w, wb, h⟩
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
⊢ ∃ w ∈ frontier s, 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
⊢ ∃ w ∈ frontier s, IsMaxOn f s w
Tactic:
exists w, wb
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
⊢ IsMaxOn f s w