internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.maximum_principle
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x r ⊆ s
Tactic:
rw [← h]
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x (Metric.infDist x sᶜ) ⊆ s
Theorem: SubharmonicOn.maximum_principle
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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
⊢ ball x (Metric.infDist x sᶜ) ⊆ s
Tactic:
apply Metric.ball_infDist_compl_subset
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle
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 : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
⊢ IsMaxOn f (closedBall x r) x
Tactic:
intro y ys
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 : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
y : ℂ
ys : y ∈ closedBall x r
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}
Theorem: SubharmonicOn.maximum_principle
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 : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
y : ℂ
ys : y ∈ closedBall x r
⊢ y ∈ {x_1 | (fun x_2 => f x_2 ≤ f x) x_1}
Tactic:
exact xm (rs ys)
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle
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 : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ f x = f w
Tactic:
apply SubharmonicOn.maximum_principle_ball (fs.mono rs) rp rm
Proof state after:
case 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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ w ∈ closedBall x r
Theorem: SubharmonicOn.maximum_principle
Proof state before:
case 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 : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
sc : IsCompact s
sn : s.Nonempty
x : ℂ
xs : x ∈ s
xm : IsMaxOn f s x
w : ℂ
wb : w ∈ frontier s
r : ℝ
h : Metric.infDist x sᶜ = r
hr : Complex.abs (w - x) = r
wx : ¬w = x
rp : r > 0
rs : closedBall x r ⊆ s
rm : IsMaxOn f (closedBall x r) x
⊢ w ∈ closedBall x r
Tactic:
simp only [Complex.dist_eq, Metric.mem_closedBall, hr, le_refl]
Proof state after:
no goals
Theorem: HarmonicOn.maximum_principle
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
sc : IsCompact s
sn : s.Nonempty
⊢ ∃ w ∈ frontier s, ∀ z ∈ s, ‖f z‖ ≤ ‖f w‖
Tactic:
rcases fh.norm.maximum_principle sc sn with ⟨w, wf, wh⟩
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
sc : IsCompact s
sn : s.Nonempty
w : ℂ
wf : w ∈ frontier s
wh : IsMaxOn (fun z => ‖f z‖) s w
⊢ ∃ w ∈ frontier s, ∀ z ∈ s, ‖f z‖ ≤ ‖f w‖
Theorem: HarmonicOn.maximum_principle
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 : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
sc : IsCompact s
sn : s.Nonempty
w : ℂ
wf : w ∈ frontier s
wh : IsMaxOn (fun z => ‖f z‖) s w
⊢ ∃ w ∈ frontier s, ∀ z ∈ s, ‖f z‖ ≤ ‖f w‖
Tactic:
exists w, wf
Proof state after:
no goals
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
⊢ ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → g c = ⨍ (t : ℝ) in itau, 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 : ℕ → ℂ → E
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ g c = ⨍ (t : ℝ) in itau, g (circleMap c r t)
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ g c = ⨍ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
have m := fun n ↦ (h n).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 : ℕ → ℂ → E
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
m : ∀ (n : ℕ), f n c = ⨍ (t : ℝ) in itau, f n (circleMap c r t)
⊢ g c = ⨍ (t : ℝ) in itau, g (circleMap c r t)
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
m : ∀ (n : ℕ), f n c = ⨍ (t : ℝ) in itau, f n (circleMap c r t)
⊢ g c = ⨍ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
simp_rw [average_eq] at m ⊢
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
m : ∀ (n : ℕ), f n c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, f n (circleMap c r t)
⊢ g c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, g (circleMap c r t)
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
m : ∀ (n : ℕ), f n c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, f n (circleMap c r t)
⊢ g c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
have se : itau =ᵐ[volume] Icc 0 (2 * π) := Ioc_ae_eq_Icc
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
m : ∀ (n : ℕ), f n c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, f n (circleMap c r t)
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
⊢ g c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, g (circleMap c r t)
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
m : ∀ (n : ℕ), f n c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, f n (circleMap c r t)
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
⊢ g c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (t : ℝ) in itau, g (circleMap c r t)
Tactic:
simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
  setIntegral_congr_set_ae se, ge_iff_le, gt_iff_lt, zero_lt_two, mul_nonneg_iff_of_pos_left,
  not_le] at m ⊢
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
m : ∀ (n : ℕ), f n c = (↑volume itau).toReal⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
⊢ g c = (↑volume itau).toReal⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
m : ∀ (n : ℕ), f n c = (↑volume itau).toReal⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
⊢ g c = (↑volume itau).toReal⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
generalize hv : (volume itau).toReal = v
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
m : ∀ (n : ℕ), f n c = (↑volume itau).toReal⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
v : ℝ
hv : (↑volume itau).toReal = v
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
m : ∀ (n : ℕ), f n c = (↑volume itau).toReal⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
v : ℝ
hv : (↑volume itau).toReal = v
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
simp_rw [hv] at m ⊢
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
v : ℝ
hv : (↑volume itau).toReal = v
m : ∀ (n : ℕ), f n c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Theorem: uniform_harmonic_lim
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
v : ℝ
hv : (↑volume itau).toReal = v
m : ∀ (n : ℕ), f n c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
clear hv
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
g : ℂ → E
s : Set ℂ
h : ∀ (n : ℕ), HarmonicOn (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
se : volume.ae.EventuallyEq itau (Icc 0 (2 * π))
v : ℝ
m : ∀ (n : ℕ), f n c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)