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
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
teu : t + e' ≤ u
e's : e' < e
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
specialize lo e' e'p e's
Proof state after:
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 z ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
⊢ (s ∩ Ioc t u).Nonempty
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 z ≤ ⨍ (t : ℝ) in itau, f (circleMap z e' t)
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rw [← hz, fz] at lo
Proof state after:
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_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ (s ∩ Ioc t u).Nonempty
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_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have ss : closedBall z e' ⊆ closedBall c r := by
  apply Metric.closedBall_subset_closedBall'; rw [Complex.dist_eq, tz]; linarith
Proof state after:
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_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
⊢ (s ∩ Ioc t u).Nonempty
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_1 : ℝ) in itau, f (circleMap (c + ↑t * y) e' t_1)
ss : closedBall z e' ⊆ closedBall c r
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have hi : ∀ x, x ∈ itau → f (circleMap z e' x) ≤ f c := by
  intro x _; apply isMaxOn_iff.mp cm; apply ss
  simp only [Complex.dist_eq, Metric.mem_closedBall, circleMap_sub_center, abs_circleMap_zero,
    abs_of_pos e'p, le_refl]
Proof state after:
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_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
⊢ (s ∩ Ioc t u).Nonempty
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_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
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have fcc : ContinuousOn (fun a ↦ f (circleMap z e' a)) itau := by
  apply (fs.cont.mono ss).comp (continuous_circleMap _ _).continuousOn; intro a _
  simp only [Complex.dist_eq, abs_of_pos e'p, Metric.mem_closedBall, circleMap_sub_center,
    abs_circleMap_zero, le_refl]
Proof state after:
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_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
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
⊢ (s ∩ Ioc t u).Nonempty
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_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
fcc : ContinuousOn (fun a => f (circleMap z e' a)) itau
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
rw [hz] at lo
Proof state after:
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
⊢ (s ∩ Ioc t u).Nonempty
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
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have fw := mean_squeeze NiceVolume.itau LocalVolume.itau fcc
  ((fs.cont.mono ss).integrableOn_sphere e'p) lo hi
Proof state after:
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
⊢ (s ∩ Ioc t u).Nonempty
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
⊢ (s ∩ Ioc t u).Nonempty
Tactic:
have eys : z + e' * y ∈ sphere z e' := by
  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:
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