Theorem: circleIntegral_sub (Ray/Analytic/Uniform.lean)

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
⊢ circleIntegral f c r - circleIntegral g c r = circleIntegral (f - g) c r
Tactic:
rw [circleIntegral]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
⊢ (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f (circleMap c r θ)) - circleIntegral g c r =
    circleIntegral (f - g) c r

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
⊢ (∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • f (circleMap c r θ)) - circleIntegral g c r =
    circleIntegral (f - g) c r
Tactic:
generalize hf : (fun θ : ℝ ↦ deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - circleIntegral g c r = circleIntegral (f - g) c r

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - circleIntegral g c r = circleIntegral (f - g) c r
Tactic:
rw [circleIntegral]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ) =
    circleIntegral (f - g) c r

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ) =
    circleIntegral (f - g) c r
Tactic:
generalize hg : (fun θ : ℝ ↦ deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = circleIntegral (f - g) c r

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = circleIntegral (f - g) c r
Tactic:
rw [circleIntegral]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • (f - g) (circleMap c r θ)

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • (f - g) (circleMap c r θ)
Tactic:
generalize hfg : (fun θ : ℝ ↦ deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume
Tactic:
have hs : fc - gc = fgc := by
  rw [← hf, ← hg, ← hfg]; funext
  simp only [deriv_circleMap, Algebra.id.smul_eq_mul, Pi.sub_apply, mul_sub_left_distrib]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume
Tactic:
rw [← hs]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume
Tactic:
clear hfg hs fgc
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume
Tactic:
symm
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
have fci := CircleIntegrable.out fi
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
rw [hf] at fci
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
have gci := CircleIntegrable.out gi
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
rw [hg] at gci
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable gc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable gc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
exact intervalIntegral.integral_sub fci gci
State after:
no goals

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ fc - gc = fgc
Tactic:
rw [← hf, ← hg, ← hfg]
State after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) =
    fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)

State before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) =
    fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)
Tactic:
funext
State after:
case h
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
x✝ : ℝ
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ))
      x✝ =
    deriv (circleMap c r) x✝ • (f - g) (circleMap c r x✝)

State before:
case h
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
x✝ : ℝ
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ))
      x✝ =
    deriv (circleMap c r) x✝ • (f - g) (circleMap c r x✝)
Tactic:
simp only [deriv_circleMap, Algebra.id.smul_eq_mul, Pi.sub_apply, mul_sub_left_distrib]
State after:
no goals