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
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + min (e / 2) (u - t) ≤ u
Tactic:
trans t + (u - t)
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
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + min (e / 2) (u - t) ≤ t + (u - t)

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
lo : ∀ (s : ℝ), 0 < s → s < e → f z ≤ ⨍ (t : ℝ) in itau, f (circleMap z s t)
e' : ℝ
he' : min (e / 2) (u - t) = e'
e'p : e' > 0
⊢ t + (u - t) ≤ u