internlm/Lean-Github huggingface dataset:
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 : ℝ
m : ∀ (n : ℕ), f n c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
t : ℝ
a✝ : t ∈ Icc 0 (2 * π)
⊢ t ∈ circleMap c r ⁻¹' s
Tactic:
simp only [Set.mem_preimage]
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)
t : ℝ
a✝ : t ∈ Icc 0 (2 * π)
⊢ circleMap c r t ∈ s
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 : ℝ
m : ∀ (n : ℕ), f n c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
t : ℝ
a✝ : t ∈ Icc 0 (2 * π)
⊢ circleMap c r t ∈ s
Tactic:
apply cs
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 : ℕ → ℂ → 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)
t : ℝ
a✝ : t ∈ Icc 0 (2 * π)
⊢ circleMap c r t ∈ closedBall c r
Theorem: uniform_harmonic_lim
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 : ℕ → ℂ → 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)
t : ℝ
a✝ : t ∈ Icc 0 (2 * π)
⊢ circleMap c r t ∈ closedBall c r
Tactic:
simp only [Complex.dist_eq, abs_of_pos rp, Metric.mem_closedBall, circleMap_sub_center,
  abs_circleMap_zero, le_refl]
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 : ℝ
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
⊢ ∀ (n : ℕ), ContinuousOn (fun t => f n (circleMap c r t)) (Icc 0 (2 * π))
Tactic:
intro n
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
⊢ ContinuousOn (fun t => f n (circleMap c r t)) (Icc 0 (2 * π))
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 : ℝ
m : ∀ (n : ℕ), f n c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), f n (circleMap c r t)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
⊢ ContinuousOn (fun t => f n (circleMap c r t)) (Icc 0 (2 * π))
Tactic:
apply Continuous.continuousOn
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
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
⊢ Continuous fun t => f n (circleMap c r t)
Theorem: uniform_harmonic_lim
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
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
⊢ Continuous fun t => f n (circleMap c r t)
Tactic:
apply ((h n).cont.mono cs).comp_continuous (continuous_circleMap _ _)
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
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
⊢ ∀ (x : ℝ), circleMap c r x ∈ closedBall c r
Theorem: uniform_harmonic_lim
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
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
⊢ ∀ (x : ℝ), circleMap c r x ∈ closedBall c r
Tactic:
intro t
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
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
t : ℝ
⊢ circleMap c r t ∈ closedBall c r
Theorem: uniform_harmonic_lim
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
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
n : ℕ
t : ℝ
⊢ circleMap c r t ∈ closedBall c r
Tactic:
simp only [Complex.dist_eq, abs_of_pos rp, Metric.mem_closedBall, circleMap_sub_center,
  abs_circleMap_zero, le_refl]
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 : ℝ
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)
cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
fu : TendstoUniformlyOn (fun n => f n ∘ circleMap c r) (g ∘ circleMap c r) atTop (Icc 0 (2 * π))
fc : ∀ (n : ℕ), ContinuousOn (fun t => f n (circleMap c r t)) (Icc 0 (2 * π))
ti :
  Tendsto (fun x => v⁻¹ • ∫ (x_1 : ℝ) in Icc 0 (2 * π), (f x ∘ circleMap c r) x_1) atTop
    (𝓝 (v⁻¹ • ∫ (x : ℝ) in Icc 0 (2 * π), (g ∘ circleMap c r) x))
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: rri
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
c : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ c + ↑r * ((↑r)⁻¹ * (z - c)) = z
Tactic:
ring_nf
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
c : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ c - c * ↑r * (↑r)⁻¹ + ↑r * (↑r)⁻¹ * z = z
Theorem: rri
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
c : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ c - c * ↑r * (↑r)⁻¹ + ↑r * (↑r)⁻¹ * z = z
Tactic:
field_simp [rp.ne']
Proof state after:
no goals
Theorem: rir
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
c : ℂ
r : ℝ
rp : r > 0
z : ℂ
⊢ (↑r)⁻¹ * (c + ↑r * z - c) = z
Tactic:
ring_nf
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
c : ℂ
r : ℝ
rp : r > 0
z : ℂ
⊢ ↑r * (↑r)⁻¹ * z = z
Theorem: rir
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
c : ℂ
r : ℝ
rp : r > 0
z : ℂ
⊢ ↑r * (↑r)⁻¹ * z = z
Tactic:
field_simp [rp.ne']
Proof state after:
no goals
Theorem: HasExtension.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
c : ℂ
r : ℝ
f0 f1 : C(Real.Angle, ℂ)
g0 g1 : ℂ → ℂ
e0 : HasExtension f0 g0 c r
e1 : HasExtension f1 g1 c r
⊢ ∀ (t : Real.Angle), (f0 - f1) t = (g0 - g1) (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
simp only [e0.b, e1.b, ContinuousMap.coe_sub, Pi.sub_apply, eq_self_iff_true,
forall_const]
Proof state after:
no goals
Theorem: mem_addCircle_iff_abs
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
c : ℂ
r : ℝ
z : ℂ
⊢ Complex.abs z = 1 ↔ ∃ t, z = ↑t.toCircle
Tactic:
constructor
Proof state after:
case mp
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
c : ℂ
r : ℝ
z : ℂ
⊢ Complex.abs z = 1 → ∃ t, z = ↑t.toCircle

case mpr
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
c : ℂ
r : ℝ
z : ℂ
⊢ (∃ t, z = ↑t.toCircle) → Complex.abs z = 1
Theorem: mem_addCircle_iff_abs
Proof state before:
case mp
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
c : ℂ
r : ℝ
z : ℂ
⊢ Complex.abs z = 1 → ∃ t, z = ↑t.toCircle
Tactic:
intro az
Proof state after:
case mp
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
c : ℂ
r : ℝ
z : ℂ
az : Complex.abs z = 1
⊢ ∃ t, z = ↑t.toCircle
Theorem: mem_addCircle_iff_abs
Proof state before:
case mp
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
c : ℂ
r : ℝ
z : ℂ
az : Complex.abs z = 1
⊢ ∃ t, z = ↑t.toCircle
Tactic:
rcases(Complex.abs_eq_one_iff z).mp az with ⟨t, h⟩
Proof state after:
case mp.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
c : ℂ
r : ℝ
z : ℂ
az : Complex.abs z = 1
t : ℝ
h : (↑t * I).exp = z
⊢ ∃ t, z = ↑t.toCircle