internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
case refine_2.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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rcases circleMap_Ioc eys with ⟨a, as, aey⟩
Proof state after:
case refine_2.intro.intro.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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
⊢ (s ∩ Ioc t u).Nonempty
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
case refine_2.intro.intro.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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
specialize fw a as
Proof state after:
case refine_2.intro.intro.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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (circleMap z e' a) = f c
⊢ (s ∩ Ioc t u).Nonempty
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
case refine_2.intro.intro.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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (circleMap z e' a) = f c
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
simp only [← aey] at fw
Proof state after:
case refine_2.intro.intro.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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ (s ∩ Ioc t u).Nonempty
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
case refine_2.intro.intro.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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
use t + e'
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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∩ Ioc t u
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 : ℝ) 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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∩ Ioc t u
Tactic:
simp only [Set.mem_inter_iff, Set.mem_Ioc, lt_add_iff_pos_right]
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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∧ 0 < e' ∧ t + e' ≤ u
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 : ℝ) 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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s ∧ 0 < e' ∧ t + e' ≤ u
Tactic:
refine ⟨?_, e'p, teu⟩
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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s
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 : ℝ) 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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ t + e' ∈ s
Tactic:
simp only [← hs, right_distrib, Set.mem_preimage, Complex.ofReal_add, Set.mem_singleton_iff]
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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ f (c + (↑t * y + ↑e' * y)) = f c
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 : ℝ) 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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ f (c + (↑t * y + ↑e' * y)) = f c
Tactic:
rw [← add_assoc, hz]
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 : ℂ → ℝ
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
eys : z + ↑e' * y ∈ sphere z e'
a : ℝ
as : a ∈ Ioc 0 (2 * π)
aey : z + ↑e' * y = circleMap z e' a
fw : f (z + ↑e' * y) = f c
⊢ f (z + ↑e' * y) = f c