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)
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
have cc : Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s := by
  rw [Set.subset_def]; intro t _; simp only [Set.mem_preimage]; apply cs
  simp only [Complex.dist_eq, abs_of_pos rp, Metric.mem_closedBall, circleMap_sub_center,
    abs_circleMap_zero, le_refl]
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
⊢ 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 : ℝ
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
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
have fu := (u.comp (circleMap c r)).mono cc
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 * π))
⊢ 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 : ℝ
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 * π))
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
have fc : ∀ n, ContinuousOn (fun t ↦ f n (circleMap c r t)) (Icc 0 (2 * π)) := by
  intro n; apply Continuous.continuousOn
  apply ((h n).cont.mono cs).comp_continuous (continuous_circleMap _ _); intro t
  simp only [Complex.dist_eq, abs_of_pos rp, Metric.mem_closedBall, circleMap_sub_center,
    abs_circleMap_zero, le_refl]
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 * π))
fc : ∀ (n : ℕ), ContinuousOn (fun t => f n (circleMap c r t)) (Icc 0 (2 * π))
⊢ 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 : ℝ
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 * π))
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
have ti' := fu.integral_tendsto fc isCompact_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
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 n => ∫ (x : ℝ) in Icc 0 (2 * π), (f n ∘ circleMap c r) x) atTop
    (𝓝 (∫ (x : ℝ) in Icc 0 (2 * π), (g ∘ circleMap c r) x))
⊢ 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 : ℝ
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 n => ∫ (x : ℝ) in Icc 0 (2 * π), (f n ∘ circleMap c r) x) atTop
    (𝓝 (∫ (x : ℝ) in Icc 0 (2 * π), (g ∘ circleMap c r) x))
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
have ti := ti'.const_smul 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 * π))
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 n => ∫ (x : ℝ) in Icc 0 (2 * π), (f n ∘ circleMap c r) x) atTop
    (𝓝 (∫ (x : ℝ) in Icc 0 (2 * π), (g ∘ circleMap c r) x))
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))
⊢ 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 : ℝ
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 n => ∫ (x : ℝ) in Icc 0 (2 * π), (f n ∘ circleMap c r) x) atTop
    (𝓝 (∫ (x : ℝ) in Icc 0 (2 * π), (g ∘ circleMap c r) x))
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))
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
clear ti'
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 * π))
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))
⊢ 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 : ℝ
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))
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
have ci := u.tendsto_at (cs (Metric.mem_closedBall_self (by linarith)))
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 * π))
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))
ci : Tendsto (fun n => f n c) atTop (𝓝 (g c))
⊢ 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 : ℝ
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))
ci : Tendsto (fun n => f n c) atTop (𝓝 (g c))
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
simp only [←m, ge_iff_le, gt_iff_lt, zero_lt_two, mul_nonneg_iff_of_pos_left, not_le,
  Function.comp_apply] at ti ⊢
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 * π))
fc : ∀ (n : ℕ), ContinuousOn (fun t => f n (circleMap c r t)) (Icc 0 (2 * π))
ci : Tendsto (fun n => f n c) atTop (𝓝 (g c))
ti : Tendsto (fun x => f x c) atTop (𝓝 (v⁻¹ • ∫ (x : ℝ) in Icc 0 (2 * π), g (circleMap c r x)))
⊢ 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 : ℝ
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 * π))
ci : Tendsto (fun n => f n c) atTop (𝓝 (g c))
ti : Tendsto (fun x => f x c) atTop (𝓝 (v⁻¹ • ∫ (x : ℝ) in Icc 0 (2 * π), g (circleMap c r x)))
⊢ g c = v⁻¹ • ∫ (t : ℝ) in Icc 0 (2 * π), g (circleMap c r t)
Tactic:
exact tendsto_nhds_unique ci ti
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)
⊢ Icc 0 (2 * π) ⊆ circleMap c r ⁻¹' s
Tactic:
rw [Set.subset_def]
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)
⊢ ∀ x ∈ Icc 0 (2 * π), x ∈ circleMap c r ⁻¹' 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)
⊢ ∀ x ∈ Icc 0 (2 * π), x ∈ circleMap c r ⁻¹' s
Tactic:
intro t _
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 * π)
⊢ t ∈ circleMap c r ⁻¹' s