internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.add
Proof state before:
case right
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
us : closedBall c u ⊆ s
⊢ f c + g c ≤ (⨍ (z : ℝ) in itau, f (circleMap c u z)) + ⨍ (z : ℝ) in itau, g (circleMap c u z)
Tactic:
have m0 := r0m u up (lt_of_lt_of_le ur (by bound))
Proof state after:
case right
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
us : closedBall c u ⊆ s
m0 : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t)
⊢ f c + g c ≤ (⨍ (z : ℝ) in itau, f (circleMap c u z)) + ⨍ (z : ℝ) in itau, g (circleMap c u z)
Theorem: SubharmonicOn.add
Proof state before:
case right
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
us : closedBall c u ⊆ s
m0 : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t)
⊢ f c + g c ≤ (⨍ (z : ℝ) in itau, f (circleMap c u z)) + ⨍ (z : ℝ) in itau, g (circleMap c u z)
Tactic:
have m1 := r1m u up (lt_of_lt_of_le ur (by bound))
Proof state after:
case right
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
us : closedBall c u ⊆ s
m0 : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t)
m1 : g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c u t)
⊢ f c + g c ≤ (⨍ (z : ℝ) in itau, f (circleMap c u z)) + ⨍ (z : ℝ) in itau, g (circleMap c u z)
Theorem: SubharmonicOn.add
Proof state before:
case right
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
us : closedBall c u ⊆ s
m0 : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t)
m1 : g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c u t)
⊢ f c + g c ≤ (⨍ (z : ℝ) in itau, f (circleMap c u z)) + ⨍ (z : ℝ) in itau, g (circleMap c u z)
Tactic:
exact add_le_add m0 m1
Proof state after:
no goals
Theorem: SubharmonicOn.add
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
⊢ min r1 r2 ≤ r1
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.add
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
⊢ min r1 r2 ≤ r2
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.add
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
⊢ 0 < r
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.add
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
⊢ r ≤ r2
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.add
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
us : closedBall c u ⊆ s
⊢ r ≤ r0
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.add
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : 0 < r0
r0m : ∀ (s : ℝ), 0 < s → s < r0 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r1 : ℝ
r1p : 0 < r1
r1m : ∀ (s : ℝ), 0 < s → s < r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
r2 : ℝ
r2p : r2 > 0
r2s : ball c r2 ⊆ interior s
r : ℝ := min r0 (min r1 r2)
rr1 : r ≤ r1
rr2 : r ≤ r2
u : ℝ
up : 0 < u
ur : u < r
us : closedBall c u ⊆ s
m0 : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t)
⊢ r ≤ r1
Tactic:
bound
Proof state after:
no goals
Theorem: HarmonicOn.neg
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
⊢ HarmonicOn (-f) s
Tactic:
have nh := HarmonicOn.sub (HarmonicOn.const 0) fh
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
nh : HarmonicOn ((fun x => 0) - f) s
⊢ HarmonicOn (-f) s
Theorem: HarmonicOn.neg
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
nh : HarmonicOn ((fun x => 0) - f) s
⊢ HarmonicOn (-f) s
Tactic:
have e : (fun _ : ℂ ↦ (0 : E)) - f = -f := by ext; simp
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
nh : HarmonicOn ((fun x => 0) - f) s
e : (fun x => 0) - f = -f
⊢ HarmonicOn (-f) s
Theorem: HarmonicOn.neg
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
nh : HarmonicOn ((fun x => 0) - f) s
e : (fun x => 0) - f = -f
⊢ HarmonicOn (-f) s
Tactic:
rwa [← e]
Proof state after:
no goals
Theorem: HarmonicOn.neg
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
nh : HarmonicOn ((fun x => 0) - f) s
⊢ (fun x => 0) - f = -f
Tactic:
ext
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
nh : HarmonicOn ((fun x => 0) - f) s
x✝ : ℂ
⊢ ((fun x => 0) - f) x✝ = (-f) x✝
Theorem: HarmonicOn.neg
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
nh : HarmonicOn ((fun x => 0) - f) s
x✝ : ℂ
⊢ ((fun x => 0) - f) x✝ = (-f) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: HarmonicOn.add
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
⊢ HarmonicOn (f + g) s
Tactic:
have e : f + g = f - -g := by ext; simp
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
e : f + g = f - -g
⊢ HarmonicOn (f + g) s
Theorem: HarmonicOn.add
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
e : f + g = f - -g
⊢ HarmonicOn (f + g) s
Tactic:
rw [e]
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
e : f + g = f - -g
⊢ HarmonicOn (f - -g) s
Theorem: HarmonicOn.add
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
e : f + g = f - -g
⊢ HarmonicOn (f - -g) s
Tactic:
exact fh.sub gh.neg
Proof state after:
no goals
Theorem: HarmonicOn.add
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
⊢ f + g = f - -g
Tactic:
ext
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
x✝ : ℂ
⊢ (f + g) x✝ = (f - -g) x✝
Theorem: HarmonicOn.add
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
x✝ : ℂ
⊢ (f + g) x✝ = (f - -g) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: HarmonicOn.const_mul
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
s : Set ℂ
fh : HarmonicOn f s
a : S
⊢ ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → a * f c = ⨍ (t : ℝ) in itau, a * f (circleMap c r t)
Tactic:
intro c r rp cs
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 : ℂ → S
s : Set ℂ
fh : HarmonicOn f s
a : S
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ a * f c = ⨍ (t : ℝ) in itau, a * f (circleMap c r t)