Theorem: uniform_harmonic_lim (Ray/Hartogs/Subharmonic.lean)

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
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)

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
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)

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 ⊢
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)

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
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)

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 ⊢
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)

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
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)

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 ⊢
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)

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
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)

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]
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)

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
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)

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]
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)

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
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)

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⁻¹
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)

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'
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)

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)))
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)

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 ⊢
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)

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
State after:
no goals

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]
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

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 _
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

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]
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

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
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

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]
State after:
no goals

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
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 * π))

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
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)

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 _ _)
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

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
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

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]
State after:
no goals

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
State after:
no goals