internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
generalize hu : Complex.abs (g - c) = u
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
have u0 : u > 0 := by
  simp only [← hu, gt_iff_lt, AbsoluteValue.pos_iff, Ne]
  contrapose gc; simp only [not_not, sub_eq_zero] at gc ⊢; exact gc
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
have ur : u ≤ r := by
  simp only [Complex.dist_eq, Metric.mem_closedBall] at gs; simp only [←hu, gs]
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
generalize hy : (g - c) / u = y
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
have y1 : abs y = 1 := by
  simp only [← hy, ← hu, map_div₀, Complex.abs_ofReal, Complex.abs_abs, ne_eq,
    Complex.abs.map_sub_eq_zero_iff, div_self (Complex.abs.ne_zero_iff.mpr (sub_ne_zero.mpr gc))]
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
generalize hs : (fun t : ℝ ↦ f (c + t * y)) ⁻¹' {f c} = s
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
have s0 : (0 : ℝ) ∈ s := by
  simp only [← hs, Set.mem_preimage, Complex.ofReal_zero, MulZeroClass.zero_mul, add_zero,
    Set.mem_singleton]
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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 : u ∈ s
⊢ f c = f g
Tactic:
simp only [← hs, ← hy, Set.mem_preimage, Set.mem_singleton_iff] at us
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 : ℂ → ℝ
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
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
have unz : (u : ℂ) ≠ 0 := by
  simp only [u0.ne', Ne, Complex.ofReal_eq_zero, not_false_iff]
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 : ℂ → ℝ
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
unz : ↑u ≠ 0
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
unz : ↑u ≠ 0
⊢ f c = f g
Tactic:
field_simp [unz] at us
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 : ℂ → ℝ
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
unz : ↑u ≠ 0
us : f g = f c
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
unz : ↑u ≠ 0
us : f g = f c
⊢ f c = f g
Tactic:
exact us.symm
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle_ball
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 : ℂ → ℝ
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
⊢ f c = f g
Tactic:
rw [gc]
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
⊢ u > 0
Tactic:
simp only [← hu, gt_iff_lt, 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 : ℂ → ℝ
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
⊢ ¬g - c = 0
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
⊢ ¬g - c = 0
Tactic:
contrapose gc
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
u : ℝ
hu : Complex.abs (g - c) = u
gc : ¬¬g - c = 0
⊢ ¬¬g = 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
u : ℝ
hu : Complex.abs (g - c) = u
gc : ¬¬g - c = 0
⊢ ¬¬g = c
Tactic:
simp only [not_not, sub_eq_zero] at gc ⊢
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
u : ℝ
hu : Complex.abs (g - c) = u
gc : g = c
⊢ g = 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
u : ℝ
hu : Complex.abs (g - c) = u
gc : g = c
⊢ g = c
Tactic:
exact gc
Proof state after:
no goals