Theorem: fubini_ball (Ray/Hartogs/FubiniBall.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (z : ℂ) in closedBall c r, f z = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have center : closedBall c r =ᵐ[volume] (closedBall c r \ {c} : Set ℂ) := ae_minus_point
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
center : volume.ae.EventuallyEq (closedBall c r) (closedBall c r \ {c})
⊢ ∫ (z : ℂ) in closedBall c r, f z = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
center : volume.ae.EventuallyEq (closedBall c r) (closedBall c r \ {c})
⊢ ∫ (z : ℂ) in closedBall c r, f z = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [MeasureTheory.setIntegral_congr_set_ae center]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
center : volume.ae.EventuallyEq (closedBall c r) (closedBall c r \ {c})
⊢ ∫ (x : ℂ) in closedBall c r \ {c}, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
center : volume.ae.EventuallyEq (closedBall c r) (closedBall c r \ {c})
⊢ ∫ (x : ℂ) in closedBall c r \ {c}, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
clear center
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (x : ℂ) in closedBall c r \ {c}, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (x : ℂ) in closedBall c r \ {c}, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [←Metric.closedBall_zero, ←annulus_oc]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (x : ℂ) in annulus_oc c 0 r, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (x : ℂ) in annulus_oc c 0 r, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
apply fubini_annulus
State after:
case fc
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ContinuousOn (fun z => f z) (annulus_cc c 0 r)

case r0p
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ 0 ≤ 0

State before:
case fc
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ContinuousOn (fun z => f z) (annulus_cc c 0 r)
Tactic:
simpa only [annulus_cc, Metric.ball_zero, diff_empty]
State after:
no goals

State before:
case r0p
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals