internlm/Lean-Github huggingface dataset:
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 ∈ interior s,
    ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
intro c 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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
c : ℂ
cs : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
rcases fs.submean' c cs with ⟨r0, r0p, r0m⟩
Proof state after:
case 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 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)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Theorem: SubharmonicOn.add
Proof state before:
case 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 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)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
rcases gs.submean' c cs with ⟨r1, r1p, r1m⟩
Proof state after:
case 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 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)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Theorem: SubharmonicOn.add
Proof state before:
case 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 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)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior c cs with ⟨r2, r2p, r2s⟩
Proof state after:
case 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 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, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Theorem: SubharmonicOn.add
Proof state before:
case 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 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, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
set r := min r0 (min r1 r2)
Proof state after:
case 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 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)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Theorem: SubharmonicOn.add
Proof state before:
case 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 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)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
have rr1 : r ≤ r1 := le_trans (min_le_right _ _) (by bound)
Proof state after:
case 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 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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Theorem: SubharmonicOn.add
Proof state before:
case 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 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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
have rr2 : r ≤ r2 := le_trans (min_le_right _ _) (by bound)
Proof state after:
case 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 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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Theorem: SubharmonicOn.add
Proof state before:
case 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 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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
use r
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 : ℂ → ℝ
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 ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Theorem: SubharmonicOn.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 : ℂ → ℝ
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 ∧ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
use 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
⊢ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
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
⊢ ∀ (s : ℝ), 0 < s → s < r → f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t) + g (circleMap c s t)
Tactic:
intro u up ur
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
⊢ f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t) + g (circleMap c u t)
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
⊢ f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t) + g (circleMap c u t)
Tactic:
have us : closedBall c u ⊆ s :=
  _root_.trans (Metric.closedBall_subset_ball (lt_of_lt_of_le ur (by bound)))
    (_root_.trans r2s interior_subset)
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
⊢ f c + g c ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t) + g (circleMap c u t)
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 ≤ ⨍ (t : ℝ) in itau, f (circleMap c u t) + g (circleMap c u t)
Tactic:
rw [Average.add ((fs.cont.mono us).integrableOn_sphere up)
    ((gs.cont.mono us).integrableOn_sphere up)]
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
⊢ f c + g c ≤ (⨍ (z : ℝ) in itau, f (circleMap c u z)) + ⨍ (z : ℝ) in itau, g (circleMap c u z)