internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ min r0 r1 > 0
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
⊢ min r0 r1 ≤ r1
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ (volume.restrict itau).ae.EventuallyEq (fun u => f (circleMap c t u)) fun u => g (circleMap c t u)
Tactic:
rw [Filter.EventuallyEq]
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict itau, f (circleMap c t x) = g (circleMap c t x)
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict itau, f (circleMap c t x) = g (circleMap c t x)
Tactic:
rw [ae_restrict_iff' measurableSet_itau]
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ itau → f (circleMap c t x) = g (circleMap c t x)
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ ∀ᵐ (x : ℝ) ∂volume, x ∈ itau → f (circleMap c t x) = g (circleMap c t x)
Tactic:
apply Filter.eventually_of_forall
Proof state after:
case hp
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ ∀ x ∈ itau, f (circleMap c t x) = g (circleMap c t x)
Theorem: SubharmonicOn.congr
Proof state before:
case hp
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ ∀ x ∈ itau, f (circleMap c t x) = g (circleMap c t x)
Tactic:
intro u _
Proof state after:
case hp
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ f (circleMap c t u) = g (circleMap c t u)
Theorem: SubharmonicOn.congr
Proof state before:
case hp
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ f (circleMap c t u) = g (circleMap c t u)
Tactic:
apply h.symm
Proof state after:
case hp.a
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ circleMap c t u ∈ s
Theorem: SubharmonicOn.congr
Proof state before:
case hp.a
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ circleMap c t u ∈ s
Tactic:
apply _root_.trans r0s interior_subset
Proof state after:
case hp.a.a
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ circleMap c t u ∈ ball c r0
Theorem: SubharmonicOn.congr
Proof state before:
case hp.a.a
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ circleMap c t u ∈ ball c r0
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq, circleMap_sub_center, abs_circleMap_zero,
  abs_of_pos tp]
Proof state after:
case hp.a.a
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ t < r0
Theorem: SubharmonicOn.congr
Proof state before:
case hp.a.a
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ t < r0
Tactic:
exact lt_of_lt_of_le tr (by bound)
Proof state after:
no goals
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
u : ℝ
a✝ : u ∈ itau
⊢ min r0 r1 ≤ r0
Tactic:
bound
Proof state after:
no goals
Theorem: HarmonicOn.const
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
a : E
s : Set ℂ
⊢ ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → a = ⨍ (t : ℝ) in itau, a
Tactic:
intro c r _ _
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
a : E
s : Set ℂ
c : ℂ
r : ℝ
a✝¹ : r > 0
a✝ : closedBall c r ⊆ s
⊢ a = ⨍ (t : ℝ) in itau, a
Theorem: HarmonicOn.const
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
a : E
s : Set ℂ
c : ℂ
r : ℝ
a✝¹ : r > 0
a✝ : closedBall c r ⊆ s
⊢ a = ⨍ (t : ℝ) in itau, a
Tactic:
rw [average_eq]
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
a : E
s : Set ℂ
c : ℂ
r : ℝ
a✝¹ : r > 0
a✝ : closedBall c r ⊆ s
⊢ a = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, a
Theorem: HarmonicOn.const
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
a : E
s : Set ℂ
c : ℂ
r : ℝ
a✝¹ : r > 0
a✝ : closedBall c r ⊆ s
⊢ a = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, a
Tactic:
simp [← smul_assoc, smul_eq_mul]
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
a : E
s : Set ℂ
c : ℂ
r : ℝ
a✝¹ : r > 0
a✝ : closedBall c r ⊆ s
⊢ a = ((↑volume itau).toReal⁻¹ * (↑volume itau).toReal) • a
Theorem: HarmonicOn.const
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
a : E
s : Set ℂ
c : ℂ
r : ℝ
a✝¹ : r > 0
a✝ : closedBall c r ⊆ s
⊢ a = ((↑volume itau).toReal⁻¹ * (↑volume itau).toReal) • a
Tactic:
field_simp [NiceVolume.itau.real_pos.ne']
Proof state after:
no goals
Theorem: HarmonicOn.sub
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
⊢ ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → (f - g) c = ⨍ (t : ℝ) in itau, (f - g) (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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (f - g) c = ⨍ (t : ℝ) in itau, (f - g) (circleMap c r t)
Theorem: HarmonicOn.sub
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
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (f - g) c = ⨍ (t : ℝ) in itau, (f - g) (circleMap c r t)
Tactic:
simp [fh.mean c r rp cs, gh.mean 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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (⨍ (t : ℝ) in itau, f (circleMap c r t)) - ⨍ (t : ℝ) in itau, g (circleMap c r t) =
    ⨍ (t : ℝ) in itau, f (circleMap c r t) - g (circleMap c r t)
Theorem: HarmonicOn.sub
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
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (⨍ (t : ℝ) in itau, f (circleMap c r t)) - ⨍ (t : ℝ) in itau, g (circleMap c r t) =
    ⨍ (t : ℝ) in itau, f (circleMap c r t) - g (circleMap c r t)
Tactic:
rw [Average.sub ((fh.cont.mono cs).integrableOn_sphere rp)
  ((gh.cont.mono cs).integrableOn_sphere rp)]
Proof state after:
no goals