internlm/Lean-Github huggingface dataset:
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
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
⊢ ∀ (x_1 : ℝ), f x (circleMap c1 r x_1) = (uncurry f ∘ fun t => (x, circleMap c1 r t)) x_1
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
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
t : ℝ
⊢ f x (circleMap c1 r t) = (uncurry f ∘ fun t => (x, circleMap c1 r t)) t
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
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
t : ℝ
⊢ f x (circleMap c1 r t) = (uncurry f ∘ fun t => (x, circleMap c1 r t)) t
Tactic:
simp
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
x : ℂ
xs : x ∈ s
comp : (fun t => f x (circleMap c1 r t)) = uncurry f ∘ fun t => (x, circleMap c1 r t)
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
Proof state before:
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
Tactic:
apply MeasureTheory.ae_of_all _
Proof state after:
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
⊢ ∀ a ∈ Ι 0 (2 * π), ContinuousWithinAt (fun x => deriv (circleMap c1 r) a • (fun z1 => f x z1) (circleMap c1 r a)) s z1
Theorem: ContinuousOn.circleIntegral
Proof state before:
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
⊢ ∀ a ∈ Ι 0 (2 * π), ContinuousWithinAt (fun x => deriv (circleMap c1 r) a • (fun z1 => f x z1) (circleMap c1 r a)) s z1
Tactic:
intro t _
Proof state after:
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 : ℝ
a✝ : 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:
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ContinuousWithinAt (fun x => deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)) s z1
Tactic:
simp
Proof state after:
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ContinuousWithinAt (fun x => (circleMap 0 r t * I) • f x (circleMap c1 r t)) s z1
Theorem: ContinuousOn.circleIntegral
Proof state before:
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ContinuousWithinAt (fun x => (circleMap 0 r t * I) • f x (circleMap c1 r t)) s z1
Tactic:
apply ContinuousOn.smul continuousOn_const
Proof state after:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ContinuousOn (fun x => f x (circleMap c1 r t)) s

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ContinuousOn (fun x => f x (circleMap c1 r t)) s

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Tactic:
have comp : (fun x ↦ f x (circleMap c1 r t)) = uncurry f ∘ fun x ↦ (x, circleMap c1 r t) := by
  apply funext; intro t; simp
Proof state after:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
⊢ ContinuousOn (fun x => f x (circleMap c1 r t)) s

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
⊢ ContinuousOn (fun x => f x (circleMap c1 r t)) s

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Tactic:
rw [comp]
Proof state after:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
⊢ ContinuousOn (uncurry f ∘ fun x => (x, circleMap c1 r t)) s

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
⊢ ContinuousOn (uncurry f ∘ fun x => (x, circleMap c1 r t)) s

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Tactic:
apply ContinuousOn.comp fc (ContinuousOn.prod continuousOn_id continuousOn_const)
Proof state after:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
⊢ Set.MapsTo (fun x => (id x, circleMap c1 r t)) s (s ×ˢ sphere c1 r)

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
⊢ Set.MapsTo (fun x => (id x, circleMap c1 r t)) s (s ×ˢ sphere c1 r)

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Tactic:
intro x xs
Proof state after:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
x : ℂ
xs : x ∈ s
⊢ (fun x => (id x, circleMap c1 r t)) x ∈ s ×ˢ sphere c1 r

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
x : ℂ
xs : x ∈ s
⊢ (fun x => (id x, circleMap c1 r t)) x ∈ s ×ˢ sphere c1 r

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Tactic:
simp
Proof state after:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
x : ℂ
xs : x ∈ s
⊢ x ∈ s ∧ 0 ≤ r

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_2.hg
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
x : ℂ
xs : x ∈ s
⊢ x ∈ s ∧ 0 ≤ r

case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Tactic:
exact ⟨xs, by linarith⟩
Proof state after:
case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_2.a
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 : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ z1 ∈ s
Tactic:
exact z1s
Proof state after:
no goals