internlm/Lean-Github huggingface dataset:
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
h : HasSum (fun n => s • ∮ (z : ℂ) in C(c, r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) g
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Tactic:
simp_rw [div_eq_mul_inv, mul_pow, ← smul_smul, circleIntegral.integral_smul, smul_comm s _] at h
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
h : HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
ci : CircleIntegrable f c r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
g : E
hg : (s • ∮ (z : ℂ) in C(c, r), (z - (c + w))⁻¹ • f z) = g
h : HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
⊢ HasSum (fun n => w ^ n • s • ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) g
Tactic:
assumption
Proof state after:
no goals
Theorem: cauchy1_hasSum
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
c w : ℂ
r : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
wm : Complex.abs w < r
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
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
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
⊢ ContinuousOn (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s
Tactic:
rcases (IsCompact.prod cs (isCompact_sphere _ _)).bddAbove_image fc.norm with ⟨b, bh⟩
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : b ∈ upperBounds ((fun x => ‖uncurry f x‖) '' s ×ˢ sphere c1 r)
⊢ ContinuousOn (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : b ∈ upperBounds ((fun x => ‖uncurry f x‖) '' s ×ˢ sphere c1 r)
⊢ ContinuousOn (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s
Tactic:
simp only [mem_upperBounds, Set.forall_mem_image] at bh
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
⊢ ContinuousOn (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
⊢ ContinuousOn (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s
Tactic:
intro z1 z1s
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
⊢ ContinuousWithinAt (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s z1
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
⊢ ContinuousWithinAt (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s z1
Tactic:
have fb : ∀ᶠ x : ℂ in 𝓝[s] z1, ∀ᵐ t : ℝ, t ∈ Set.uIoc 0 (2 * π) →
    ‖deriv (circleMap c1 r) t • (fun z1 : ℂ ↦ f x z1) (circleMap c1 r t)‖ ≤ r * b := by
  apply eventually_nhdsWithin_of_forall; intro x xs
  apply MeasureTheory.ae_of_all _; intro t _; simp only [deriv_circleMap]
  rw [norm_smul, Complex.norm_eq_abs]
  simp only [map_mul, abs_circleMap_zero, Complex.abs_I, mul_one]
  have bx := @bh (x, circleMap c1 r t) (Set.mk_mem_prod xs (circleMap_mem_sphere c1
    (by linarith) t))
  simp only [uncurry] at bx
  calc |r| * ‖f x (circleMap c1 r t)‖ ≤ |r| * b := by bound
    _ = r * b := by rw [abs_of_pos rp]
Proof state after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ ContinuousWithinAt (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s z1
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ ContinuousWithinAt (fun z0 => ∮ (z1 : ℂ) in C(c1, r), f z0 z1) s z1
Tactic:
refine intervalIntegral.continuousWithinAt_of_dominated_interval ?_ fb (by simp) ?_
Proof state after:
case intro.refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    MeasureTheory.AEStronglyMeasurable (fun θ => deriv (circleMap c1 r) θ • (fun z1 => f x z1) (circleMap c1 r θ))
      (MeasureTheory.volume.restrict (Ι 0 (2 * π)))

case intro.refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume,
    t ∈ Ι 0 (2 * π) →
      ContinuousWithinAt (fun x => deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)) s z1
Theorem: ContinuousOn.circleIntegral
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
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
⊢ ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
Tactic:
apply eventually_nhdsWithin_of_forall
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
⊢ ∀ x ∈ s, ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
⊢ ∀ x ∈ s, ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
Tactic:
intro x xs
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
⊢ ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
Tactic:
apply MeasureTheory.ae_of_all _
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
⊢ ∀ a ∈ Ι 0 (2 * π), ‖deriv (circleMap c1 r) a • (fun z1 => f x z1) (circleMap c1 r a)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
⊢ ∀ a ∈ Ι 0 (2 * π), ‖deriv (circleMap c1 r) a • (fun z1 => f x z1) (circleMap c1 r a)‖ ≤ r * b
Tactic:
intro t _
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
Tactic:
simp only [deriv_circleMap]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ‖(circleMap 0 r t * I) • f x (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ‖(circleMap 0 r t * I) • f x (circleMap c1 r t)‖ ≤ r * b
Tactic:
rw [norm_smul, Complex.norm_eq_abs]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ Complex.abs (circleMap 0 r t * I) * ‖f x (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ Complex.abs (circleMap 0 r t * I) * ‖f x (circleMap c1 r t)‖ ≤ r * b
Tactic:
simp only [map_mul, abs_circleMap_zero, Complex.abs_I, mul_one]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ |r| * ‖f x (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ |r| * ‖f x (circleMap c1 r t)‖ ≤ r * b
Tactic:
have bx := @bh (x, circleMap c1 r t) (Set.mk_mem_prod xs (circleMap_mem_sphere c1
  (by linarith) t))
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
bx : ‖uncurry f (x, circleMap c1 r t)‖ ≤ b
⊢ |r| * ‖f x (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
bx : ‖uncurry f (x, circleMap c1 r t)‖ ≤ b
⊢ |r| * ‖f x (circleMap c1 r t)‖ ≤ r * b
Tactic:
simp only [uncurry] at bx
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
bx : ‖f x (circleMap c1 r t)‖ ≤ b
⊢ |r| * ‖f x (circleMap c1 r t)‖ ≤ r * b
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
bx : ‖f x (circleMap c1 r t)‖ ≤ b
⊢ |r| * ‖f x (circleMap c1 r t)‖ ≤ r * b
Tactic:
calc |r| * ‖f x (circleMap c1 r t)‖ ≤ |r| * b := by bound
  _ = r * b := by rw [abs_of_pos rp]
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
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
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
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
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
bx : ‖f x (circleMap c1 r t)‖ ≤ b
⊢ |r| * ‖f x (circleMap c1 r t)‖ ≤ |r| * b
Tactic:
bound
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
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
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
x : ℂ
xs : x ∈ s
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
bx : ‖f x (circleMap c1 r t)‖ ≤ b
⊢ |r| * b = r * b
Tactic:
rw [abs_of_pos rp]
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
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
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ IntervalIntegrable (fun t => r * b) MeasureTheory.volume 0 (2 * π)
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    MeasureTheory.AEStronglyMeasurable (fun θ => deriv (circleMap c1 r) θ • (fun z1 => f x z1) (circleMap c1 r θ))
      (MeasureTheory.volume.restrict (Ι 0 (2 * π)))
Tactic:
apply eventually_nhdsWithin_of_forall
Proof state after:
case intro.refine_1.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ ∀ x ∈ s,
    MeasureTheory.AEStronglyMeasurable (fun θ => deriv (circleMap c1 r) θ • (fun z1 => f x z1) (circleMap c1 r θ))
      (MeasureTheory.volume.restrict (Ι 0 (2 * π)))
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_1.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
⊢ ∀ x ∈ s,
    MeasureTheory.AEStronglyMeasurable (fun θ => deriv (circleMap c1 r) θ • (fun z1 => f x z1) (circleMap c1 r θ))
      (MeasureTheory.volume.restrict (Ι 0 (2 * π)))
Tactic:
intro x xs
Proof state after:
case intro.refine_1.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
x : ℂ
xs : x ∈ s
⊢ MeasureTheory.AEStronglyMeasurable (fun θ => deriv (circleMap c1 r) θ • (fun z1 => f x z1) (circleMap c1 r θ))
    (MeasureTheory.volume.restrict (Ι 0 (2 * π)))