internlm/Lean-Github huggingface dataset:
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact Continuous.sub (Continuous.snd continuous_id) continuous_const
Proof state after:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
intro x xp
Proof state after:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact center_not_in_sphere rp (Set.mem_prod.mp xp).right
Proof state after:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
simp
Proof state after:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f x) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f x) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact fc
Proof state after:
no goals
Theorem: sum_integral_commute
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, r), f n z) (∮ (z : ℂ) in C(c, r), g z)
Tactic:
rw [circleIntegral]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, r), f n z) (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ))
Theorem: sum_integral_commute
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, r), f n z) (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ))
Tactic:
simp_rw [circleIntegral]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ HasSum (fun n => ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f n (circleMap c r θ))
    (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ))
Theorem: sum_integral_commute
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ HasSum (fun n => ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f n (circleMap c r θ))
    (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ))
Tactic:
simp
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ HasSum (fun n => ∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f n (circleMap c r θ))
    (∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • g (circleMap c r θ))
Theorem: sum_integral_commute
Proof state before:
case hF_meas
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ ∀ (n : ℕ),
    MeasureTheory.AEStronglyMeasurable (fun t => (circleMap 0 r t * I) • f n (circleMap c r t))
      (MeasureTheory.volume.restrict (Ι 0 (2 * π)))
Tactic:
intro n
Proof state after:
case hF_meas
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasureTheory.AEStronglyMeasurable (fun t => (circleMap 0 r t * I) • f n (circleMap c r t))
    (MeasureTheory.volume.restrict (Ι 0 (2 * π)))
Theorem: sum_integral_commute
Proof state before:
case hF_meas
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasureTheory.AEStronglyMeasurable (fun t => (circleMap 0 r t * I) • f n (circleMap c r t))
    (MeasureTheory.volume.restrict (Ι 0 (2 * π)))
Tactic:
apply ContinuousOn.aestronglyMeasurable
Proof state after:
case hF_meas.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun t => (circleMap 0 r t * I) • f n (circleMap c r t)) (Ι 0 (2 * π))

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Theorem: sum_integral_commute
Proof state before:
case hF_meas.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun t => (circleMap 0 r t * I) • f n (circleMap c r t)) (Ι 0 (2 * π))

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Tactic:
apply ContinuousOn.smul
Proof state after:
case hF_meas.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun x => circleMap 0 r x * I) (Ι 0 (2 * π))

case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun x => f n (circleMap c r x)) (Ι 0 (2 * π))

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Theorem: sum_integral_commute
Proof state before:
case hF_meas.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun x => circleMap 0 r x * I) (Ι 0 (2 * π))

case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun x => f n (circleMap c r x)) (Ι 0 (2 * π))

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Tactic:
apply ContinuousOn.mul (Continuous.continuousOn (continuous_circleMap _ _)) continuousOn_const
Proof state after:
case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun x => f n (circleMap c r x)) (Ι 0 (2 * π))

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Theorem: sum_integral_commute
Proof state before:
case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ContinuousOn (fun x => f n (circleMap c r x)) (Ι 0 (2 * π))

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Tactic:
apply ContinuousOn.comp (fc n) (Continuous.continuousOn (continuous_circleMap _ _))
Proof state after:
case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ Set.MapsTo (circleMap c r) (Ι 0 (2 * π)) (sphere c r)

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Theorem: sum_integral_commute
Proof state before:
case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ Set.MapsTo (circleMap c r) (Ι 0 (2 * π)) (sphere c r)

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Tactic:
intro t _
Proof state after:
case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ circleMap c r t ∈ sphere c r

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Theorem: sum_integral_commute
Proof state before:
case hF_meas.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ circleMap c r t ∈ sphere c r

case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Tactic:
exact circleMap_mem_sphere _ (by linarith) _
Proof state after:
case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Theorem: sum_integral_commute
Proof state before:
case hF_meas.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ MeasurableSet (Ι 0 (2 * π))
Tactic:
exact measurableSet_uIoc
Proof state after:
no goals
Theorem: sum_integral_commute
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: sum_integral_commute
Proof state before:
case h_bound
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
⊢ ∀ (n : ℕ),
    ∀ᵐ (t : ℝ) ∂MeasureTheory.volume, t ∈ Ι 0 (2 * π) → ‖(circleMap 0 r t * I) • f n (circleMap c r t)‖ ≤ r * b n
Tactic:
intro n
Proof state after:
case h_bound
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume, t ∈ Ι 0 (2 * π) → ‖(circleMap 0 r t * I) • f n (circleMap c r t)‖ ≤ r * b n
Theorem: sum_integral_commute
Proof state before:
case h_bound
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume, t ∈ Ι 0 (2 * π) → ‖(circleMap 0 r t * I) • f n (circleMap c r t)‖ ≤ r * b n
Tactic:
apply MeasureTheory.ae_of_all
Proof state after:
case h_bound.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℕ → ℂ → E
g : ℂ → E
c : ℂ
r : ℝ
b : ℕ → ℝ
rp : r > 0
fc : ∀ (n : ℕ), ContinuousOn (f n) (sphere c r)
fb : ∀ (n : ℕ), ∀ z ∈ sphere c r, ‖f n z‖ ≤ b n
bs : Summable b
h : ∀ z ∈ sphere c r, HasSum (fun n => f n z) (g z)
n : ℕ
⊢ ∀ a ∈ Ι 0 (2 * π), ‖(circleMap 0 r a * I) • f n (circleMap c r a)‖ ≤ r * b n