internlm/Lean-Github huggingface dataset:
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Tactic:
have im := intervalIntegral.integral_mono_on nonneg_2π i0 i1 mo
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 : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
im : ∫ (u : ℝ) in 0 ..2 * π, ‖f (circleMap c r u)‖ ≤ ∫ (u : ℝ) in 0 ..2 * π, b
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
im : ∫ (u : ℝ) in 0 ..2 * π, ‖f (circleMap c r u)‖ ≤ ∫ (u : ℝ) in 0 ..2 * π, b
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Tactic:
simp only [integral_const, sub_zero, smul_eq_mul] at im
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 : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
im : ∫ (u : ℝ) in 0 ..2 * π, ‖f (circleMap c r u)‖ ≤ 2 * π * b
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
im : ∫ (u : ℝ) in 0 ..2 * π, ‖f (circleMap c r u)‖ ≤ 2 * π * b
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Tactic:
calc |r| * ∫ t in (0)..(2*π), ‖f (circleMap c r t)‖
  _ ≤ |r| * (2 * π * b) := by bound
  _ = r * (2 * π * b) := by rw [abs_of_pos rp]
  _ = 2 * π * r * b := by ring
Proof state after:
no goals
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
t : ℝ
x✝ : t ∈ Set.Icc 0 (2 * π)
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
⊢ IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
Tactic:
apply ContinuousOn.intervalIntegrable
Proof state after:
case hu
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
⊢ ContinuousOn (fun t => ‖f (circleMap c r t)‖) (Set.uIcc 0 (2 * π))
Theorem: bounded_circleIntegral
Proof state before:
case hu
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
⊢ ContinuousOn (fun t => ‖f (circleMap c r t)‖) (Set.uIcc 0 (2 * π))
Tactic:
have ca : ContinuousOn (norm : E → ℝ) Set.univ := Continuous.continuousOn continuous_norm
Proof state after:
case hu
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ ContinuousOn (fun t => ‖f (circleMap c r t)‖) (Set.uIcc 0 (2 * π))
Theorem: bounded_circleIntegral
Proof state before:
case hu
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ ContinuousOn (fun t => ‖f (circleMap c r t)‖) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.comp ca ?_ (Set.mapsTo_univ _ _)
Proof state after:
case hu
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ ContinuousOn (fun t => f (circleMap c r t)) (Set.uIcc 0 (2 * π))
Theorem: bounded_circleIntegral
Proof state before:
case hu
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ ContinuousOn (fun t => f (circleMap c r t)) (Set.uIcc 0 (2 * π))
Tactic:
apply ContinuousOn.comp fc
Proof state after:
case hu.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ ContinuousOn (fun t => circleMap c r t) (Set.uIcc 0 (2 * π))

case hu.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ Set.MapsTo (fun t => circleMap c r t) (Set.uIcc 0 (2 * π)) (sphere c r)
Theorem: bounded_circleIntegral
Proof state before:
case hu.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ ContinuousOn (fun t => circleMap c r t) (Set.uIcc 0 (2 * π))

case hu.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ Set.MapsTo (fun t => circleMap c r t) (Set.uIcc 0 (2 * π)) (sphere c r)
Tactic:
exact Continuous.continuousOn (continuous_circleMap _ _)
Proof state after:
case hu.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ Set.MapsTo (fun t => circleMap c r t) (Set.uIcc 0 (2 * π)) (sphere c r)
Theorem: bounded_circleIntegral
Proof state before:
case hu.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
⊢ Set.MapsTo (fun t => circleMap c r t) (Set.uIcc 0 (2 * π)) (sphere c r)
Tactic:
intro t _
Proof state after:
case hu.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
t : ℝ
a✝ : t ∈ Set.uIcc 0 (2 * π)
⊢ (fun t => circleMap c r t) t ∈ sphere c r
Theorem: bounded_circleIntegral
Proof state before:
case hu.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b✝ : ℝ
f : ℂ → E
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
t : ℝ
a✝ : t ∈ Set.uIcc 0 (2 * π)
⊢ (fun t => circleMap c r t) t ∈ sphere c r
Tactic:
exact circleMap_mem_sphere _ (by linarith) _
Proof state after:
no goals
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
ca : ContinuousOn norm Set.univ
t : ℝ
a✝ : t ∈ Set.uIcc 0 (2 * π)
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
im : ∫ (u : ℝ) in 0 ..2 * π, ‖f (circleMap c r u)‖ ≤ 2 * π * b
⊢ |r| * ∫ (t : ℝ) in 0 ..2 * π, ‖f (circleMap c r t)‖ ≤ |r| * (2 * π * b)
Tactic:
bound
Proof state after:
no goals
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
im : ∫ (u : ℝ) in 0 ..2 * π, ‖f (circleMap c r u)‖ ≤ 2 * π * b
⊢ |r| * (2 * π * b) = r * (2 * π * b)
Tactic:
rw [abs_of_pos rp]
Proof state after:
no goals
Theorem: bounded_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
c : ℂ
r b : ℝ
rp : r > 0
fc : ContinuousOn f (sphere c r)
fb : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
nonneg_2π : 0 ≤ 2 * π
mo : ∀ t ∈ Set.Icc 0 (2 * π), ‖f (circleMap c r t)‖ ≤ b
i0 : IntervalIntegrable (fun t => ‖f (circleMap c r t)‖) MeasureTheory.volume 0 (2 * π)
i1 : IntervalIntegrable (fun x => b) MeasureTheory.volume 0 (2 * π)
im : ∫ (u : ℝ) in 0 ..2 * π, ‖f (circleMap c r u)‖ ≤ 2 * π * b
⊢ r * (2 * π * b) = 2 * π * r * b
Tactic:
ring
Proof state after:
no goals
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * b * r⁻¹ ^ n
Tactic:
have sb : ∀ z, z ∈ sphere c r → ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b := by
  intro z zs; have fb := bh z zs
  rw [norm_smul, norm_smul, Complex.norm_eq_abs, Complex.norm_eq_abs]
  simp only [inv_pow, map_inv₀, map_pow, ge_iff_le, Metric.mem_sphere, Complex.dist_eq] at zs ⊢
  rw [zs]; ring_nf; bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * b * r⁻¹ ^ n
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * b * r⁻¹ ^ n
Tactic:
have isb := bounded_circleIntegral rp ?_ sb
Proof state after:
case 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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
isb : ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b)
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * b * r⁻¹ ^ n

case 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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
⊢ ContinuousOn (fun z => (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) (sphere c r)
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
⊢ ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
Tactic:
intro z zs
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
zs : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
zs : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
Tactic:
have fb := bh z zs
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
zs : z ∈ sphere c r
fb : ‖f z‖ ≤ b
⊢ ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
zs : z ∈ sphere c r
fb : ‖f z‖ ≤ b
⊢ ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
Tactic:
rw [norm_smul, norm_smul, Complex.norm_eq_abs, Complex.norm_eq_abs]
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
zs : z ∈ sphere c r
fb : ‖f z‖ ≤ b
⊢ Complex.abs ((z - c)⁻¹ ^ n) * (Complex.abs (z - c)⁻¹ * ‖f z‖) ≤ r⁻¹ ^ n * r⁻¹ * b
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
zs : z ∈ sphere c r
fb : ‖f z‖ ≤ b
⊢ Complex.abs ((z - c)⁻¹ ^ n) * (Complex.abs (z - c)⁻¹ * ‖f z‖) ≤ r⁻¹ ^ n * r⁻¹ * b
Tactic:
simp only [inv_pow, map_inv₀, map_pow, ge_iff_le, Metric.mem_sphere, Complex.dist_eq] at zs ⊢
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
fb : ‖f z‖ ≤ b
zs : Complex.abs (z - c) = r
⊢ (Complex.abs (z - c) ^ n)⁻¹ * ((Complex.abs (z - c))⁻¹ * ‖f z‖) ≤ (r ^ n)⁻¹ * r⁻¹ * b
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
fb : ‖f z‖ ≤ b
zs : Complex.abs (z - c) = r
⊢ (Complex.abs (z - c) ^ n)⁻¹ * ((Complex.abs (z - c))⁻¹ * ‖f z‖) ≤ (r ^ n)⁻¹ * r⁻¹ * b
Tactic:
rw [zs]
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
fb : ‖f z‖ ≤ b
zs : Complex.abs (z - c) = r
⊢ (r ^ n)⁻¹ * (r⁻¹ * ‖f z‖) ≤ (r ^ n)⁻¹ * r⁻¹ * b
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
fb : ‖f z‖ ≤ b
zs : Complex.abs (z - c) = r
⊢ (r ^ n)⁻¹ * (r⁻¹ * ‖f z‖) ≤ (r ^ n)⁻¹ * r⁻¹ * b
Tactic:
ring_nf
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
fb : ‖f z‖ ≤ b
zs : Complex.abs (z - c) = r
⊢ r⁻¹ * r⁻¹ ^ n * ‖f z‖ ≤ r⁻¹ * r⁻¹ ^ n * b
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
z : ℂ
fb : ‖f z‖ ≤ b
zs : Complex.abs (z - c) = r
⊢ r⁻¹ * r⁻¹ ^ n * ‖f z‖ ≤ r⁻¹ * r⁻¹ ^ n * b
Tactic:
bound
Proof state after:
no goals
Theorem: cauchy1_bound
Proof state before:
case 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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
isb : ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b)
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * b * r⁻¹ ^ n
Tactic:
calc ‖∮ z in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖
  _ ≤ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b) := isb
  _ = 2 * π * b * r⁻¹ ^ n * (r * r⁻¹) := by ring
  _ = 2 * π * b * r⁻¹ ^ n := by rw [mul_inv_cancel rp.ne']; simp
Proof state after:
no goals
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
isb : ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b)
⊢ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b) = 2 * π * b * r⁻¹ ^ n * (r * r⁻¹)
Tactic:
ring
Proof state after:
no goals
Theorem: cauchy1_bound
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
isb : ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b)
⊢ 2 * π * b * r⁻¹ ^ n * (r * r⁻¹) = 2 * π * b * r⁻¹ ^ n
Tactic:
rw [mul_inv_cancel rp.ne']
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
b r : ℝ
c : ℂ
rp : r > 0
fc : ContinuousOn f (sphere c r)
bh : ∀ z ∈ sphere c r, ‖f z‖ ≤ b
n : ℕ
sb : ∀ z ∈ sphere c r, ‖(z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ r⁻¹ ^ n * r⁻¹ * b
isb : ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖ ≤ 2 * π * r * (r⁻¹ ^ n * r⁻¹ * b)
⊢ 2 * π * b * r⁻¹ ^ n * 1 = 2 * π * b * r⁻¹ ^ n