Theorem: bounded_circleIntegral (Ray/Hartogs/Osgood.lean)

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
⊢ ‖∮ (z : ℂ) in C(c, r), f z‖ ≤ 2 * π * r * b
Tactic:
rw [circleIntegral]
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
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f (circleMap c r θ)‖ ≤ 2 * π * r * b

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
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f (circleMap c r θ)‖ ≤ 2 * π * r * b
Tactic:
simp only [deriv_circleMap]
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
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f (circleMap c r θ)‖ ≤ 2 * π * r * b

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
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f (circleMap c r θ)‖ ≤ 2 * π * r * b
Tactic:
have nonneg_2π := Real.two_pi_pos.le
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 * π
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f (circleMap c r θ)‖ ≤ 2 * π * r * b

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 * π
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f (circleMap c r θ)‖ ≤ 2 * π * r * b
Tactic:
have ib : ‖(∫ t in (0)..(2*π), (circleMap 0 r t * I) • f (circleMap c r t))‖ ≤
    (∫ t in (0)..(2*π), ‖(circleMap 0 r t * I) • f (circleMap c r t)‖) :=
  intervalIntegral.norm_integral_le_integral_norm nonneg_2π
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 * π
ib :
  ‖∫ (t : ℝ) in 0 ..2 * π, (circleMap 0 r t * I) • f (circleMap c r t)‖ ≤
    ∫ (t : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f (circleMap c r θ)‖ ≤ 2 * π * r * b

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 * π
ib :
  ‖∫ (t : ℝ) in 0 ..2 * π, (circleMap 0 r t * I) • f (circleMap c r t)‖ ≤
    ∫ (t : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖
⊢ ‖∫ (θ : ℝ) in 0 ..2 * π, (circleMap 0 r θ * I) • f (circleMap c r θ)‖ ≤ 2 * π * r * b
Tactic:
refine le_trans ib ?_
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 * π
ib :
  ‖∫ (t : ℝ) in 0 ..2 * π, (circleMap 0 r t * I) • f (circleMap c r t)‖ ≤
    ∫ (t : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖
⊢ ∫ (t : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖ ≤ 2 * π * r * b

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 * π
ib :
  ‖∫ (t : ℝ) in 0 ..2 * π, (circleMap 0 r t * I) • f (circleMap c r t)‖ ≤
    ∫ (t : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖
⊢ ∫ (t : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖ ≤ 2 * π * r * b
Tactic:
clear ib
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 * π
⊢ ∫ (t : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖ ≤ 2 * π * r * b

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 : ℝ) in 0 ..2 * π, ‖(circleMap 0 r t * I) • f (circleMap c r t)‖ ≤ 2 * π * r * b
Tactic:
simp_rw [norm_smul, Complex.norm_eq_abs]
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 * π
⊢ ∫ (t : ℝ) in 0 ..2 * π, Complex.abs (circleMap 0 r t * I) * ‖f (circleMap c r t)‖ ≤ 2 * π * r * b

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 : ℝ) in 0 ..2 * π, Complex.abs (circleMap 0 r t * I) * ‖f (circleMap c r t)‖ ≤ 2 * π * r * b
Tactic:
simp only [map_mul, abs_circleMap_zero, Complex.abs_I, mul_one, integral_const_mul]
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 * π
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b

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 * π
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Tactic:
have mo : ∀ t, t ∈ Set.Icc 0 (2 * π) → ‖f (circleMap c r t)‖ ≤ b := fun t _ ↦
  fb (circleMap c r t) (circleMap_mem_sphere c (by linarith) t)
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
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b

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
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Tactic:
have i0 : IntervalIntegrable (fun t ↦ ‖f (circleMap c r t)‖) Real.measureSpace.volume
    0 (2*π) := by
  apply ContinuousOn.intervalIntegrable
  have ca : ContinuousOn (norm : E → ℝ) Set.univ := Continuous.continuousOn continuous_norm
  refine ContinuousOn.comp ca ?_ (Set.mapsTo_univ _ _)
  apply ContinuousOn.comp fc
  exact Continuous.continuousOn (continuous_circleMap _ _)
  intro t _; exact circleMap_mem_sphere _ (by linarith) _
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 * π)
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b

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 * π)
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b
Tactic:
have i1 : IntervalIntegrable (fun _ ↦ b) Real.measureSpace.volume 0 (2 * π) :=
  intervalIntegrable_const
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 * π)
⊢ |r| * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c r x)‖ ≤ 2 * π * r * b

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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