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

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (z : ℂ) in annulus_oc c r0 r1, f z = ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have im := MeasurePreserving.symm _ Complex.volume_preserving_equiv_real_prod
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
im : MeasurePreserving (⇑Complex.measurableEquivRealProd.symm) volume volume
⊢ ∫ (z : ℂ) in annulus_oc c r0 r1, f z = ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
im : MeasurePreserving (⇑Complex.measurableEquivRealProd.symm) volume volume
⊢ ∫ (z : ℂ) in annulus_oc c r0 r1, f z = ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [←MeasurePreserving.setIntegral_preimage_emb im
  Complex.measurableEquivRealProd.symm.measurableEmbedding f _]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
im : MeasurePreserving (⇑Complex.measurableEquivRealProd.symm) volume volume
⊢ ∫ (x : ℝ × ℝ) in ⇑Complex.measurableEquivRealProd.symm ⁻¹' annulus_oc c r0 r1,
      f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
im : MeasurePreserving (⇑Complex.measurableEquivRealProd.symm) volume volume
⊢ ∫ (x : ℝ × ℝ) in ⇑Complex.measurableEquivRealProd.symm ⁻¹' annulus_oc c r0 r1,
      f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
clear im
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in ⇑Complex.measurableEquivRealProd.symm ⁻¹' annulus_oc c r0 r1,
      f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in ⇑Complex.measurableEquivRealProd.symm ⁻¹' annulus_oc c r0 r1,
      f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [square_eq r0p]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in realCircleMap c '' square r0 r1, f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in realCircleMap c '' square r0 r1, f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have dc : ∀ x, x ∈ square r0 r1 →
    HasFDerivWithinAt (realCircleMap c) (rcmDeriv x) (square r0 r1) x :=
  fun _ _ ↦ realCircleMap.fderiv.hasFDerivWithinAt
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
dc : ∀ x ∈ square r0 r1, HasFDerivWithinAt (realCircleMap c) (rcmDeriv x) (square r0 r1) x
⊢ ∫ (x : ℝ × ℝ) in realCircleMap c '' square r0 r1, f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
dc : ∀ x ∈ square r0 r1, HasFDerivWithinAt (realCircleMap c) (rcmDeriv x) (square r0 r1) x
⊢ ∫ (x : ℝ × ℝ) in realCircleMap c '' square r0 r1, f (Complex.measurableEquivRealProd.symm x) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [integral_image_eq_integral_abs_det_fderiv_smul volume Measurable.square dc (rcm_inj r0p)]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
dc : ∀ x ∈ square r0 r1, HasFDerivWithinAt (realCircleMap c) (rcmDeriv x) (square r0 r1) x
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |(rcmDeriv x).det| • f (Complex.measurableEquivRealProd.symm (realCircleMap c x)) =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
dc : ∀ x ∈ square r0 r1, HasFDerivWithinAt (realCircleMap c) (rcmDeriv x) (square r0 r1) x
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |(rcmDeriv x).det| • f (Complex.measurableEquivRealProd.symm (realCircleMap c x)) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
clear dc
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |(rcmDeriv x).det| • f (Complex.measurableEquivRealProd.symm (realCircleMap c x)) =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |(rcmDeriv x).det| • f (Complex.measurableEquivRealProd.symm (realCircleMap c x)) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
simp_rw [rcmDeriv.det]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |x.1| • f (Complex.measurableEquivRealProd.symm (realCircleMap c x)) =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |x.1| • f (Complex.measurableEquivRealProd.symm (realCircleMap c x)) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
simp_rw [realCircleMap_eq_circleMap]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1,
      |x.1| • f (Complex.measurableEquivRealProd.symm (Complex.equivRealProd (circleMap c x.1 x.2))) =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1,
      |x.1| • f (Complex.measurableEquivRealProd.symm (Complex.equivRealProd (circleMap c x.1 x.2))) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
simp_rw [measurable_symm_equiv_inverse]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |x.1| • f (circleMap c x.1 x.2) =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |x.1| • f (circleMap c x.1 x.2) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have e : ∀ x : ℝ × ℝ, x ∈ square r0 r1 → |x.1| • f (circleMap c x.1 x.2) =
    x.1 • f (circleMap c x.1 x.2) := by
  intro x xs; rw [abs_of_pos (square.rp r0p xs)]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
e : ∀ x ∈ square r0 r1, |x.1| • f (circleMap c x.1 x.2) = x.1 • f (circleMap c x.1 x.2)
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |x.1| • f (circleMap c x.1 x.2) =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
e : ∀ x ∈ square r0 r1, |x.1| • f (circleMap c x.1 x.2) = x.1 • f (circleMap c x.1 x.2)
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, |x.1| • f (circleMap c x.1 x.2) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [MeasureTheory.setIntegral_congr Measurable.square e]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
e : ∀ x ∈ square r0 r1, |x.1| • f (circleMap c x.1 x.2) = x.1 • f (circleMap c x.1 x.2)
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, x.1 • f (circleMap c x.1 x.2) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
e : ∀ x ∈ square r0 r1, |x.1| • f (circleMap c x.1 x.2) = x.1 • f (circleMap c x.1 x.2)
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, x.1 • f (circleMap c x.1 x.2) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
clear e
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, x.1 • f (circleMap c x.1 x.2) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, 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 : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ × ℝ) in square r0 r1, x.1 • f (circleMap c x.1 x.2) ∂volume =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [square, Measure.volume_eq_prod, MeasureTheory.setIntegral_prod]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ) in Ioc r0 r1, ∫ (y : ℝ) in Ioc 0 (2 * π), (x, y).1 • f (circleMap c (x, y).1 (x, y).2) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ IntegrableOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Ioc r0 r1 ×ˢ Ioc 0 (2 * π)) (volume.prod volume)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∫ (x : ℝ) in Ioc r0 r1, ∫ (y : ℝ) in Ioc 0 (2 * π), (x, y).1 • f (circleMap c (x, y).1 (x, y).2) =
    ∫ (s : ℝ) in Ioc r0 r1, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ IntegrableOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Ioc r0 r1 ×ˢ Ioc 0 (2 * π)) (volume.prod volume)
Tactic:
simp [integral_smul]
State after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ IntegrableOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Ioc r0 r1 ×ˢ Ioc 0 (2 * π)) (volume.prod volume)

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
fi : IntegrableOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Icc r0 r1 ×ˢ Icc 0 (2 * π)) volume
⊢ IntegrableOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Ioc r0 r1 ×ˢ Ioc 0 (2 * π)) (volume.prod volume)
Tactic:
exact fi.mono_set (prod_mono Ioc_subset_Icc_self Ioc_subset_Icc_self)
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ∀ x ∈ square r0 r1, |x.1| • f (circleMap c x.1 x.2) = x.1 • f (circleMap c x.1 x.2)
Tactic:
intro x xs
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : x ∈ square r0 r1
⊢ |x.1| • f (circleMap c x.1 x.2) = x.1 • f (circleMap c x.1 x.2)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : x ∈ square r0 r1
⊢ |x.1| • f (circleMap c x.1 x.2) = x.1 • f (circleMap c x.1 x.2)
Tactic:
rw [abs_of_pos (square.rp r0p xs)]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ IntegrableOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Icc r0 r1 ×ˢ Icc 0 (2 * π)) volume
Tactic:
apply ContinuousOn.integrableOn_compact
State after:
case hK
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ IsCompact (Icc r0 r1 ×ˢ Icc 0 (2 * π))

case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ContinuousOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Icc r0 r1 ×ˢ Icc 0 (2 * π))

State before:
case hK
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ IsCompact (Icc r0 r1 ×ˢ Icc 0 (2 * π))
Tactic:
exact IsCompact.prod isCompact_Icc isCompact_Icc
State after:
no goals

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ContinuousOn (fun x => x.1 • f (circleMap c x.1 x.2)) (Icc r0 r1 ×ˢ Icc 0 (2 * π))
Tactic:
apply ContinuousOn.smul continuous_fst.continuousOn
State after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ContinuousOn (fun x => f (circleMap c x.1 x.2)) (Icc r0 r1 ×ˢ Icc 0 (2 * π))

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ ContinuousOn (fun x => f (circleMap c x.1 x.2)) (Icc r0 r1 ×ˢ Icc 0 (2 * π))
Tactic:
apply fc.comp continuous_circleMap_full.continuousOn
State after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ MapsTo (fun x => circleMap c x.1 x.2) (Icc r0 r1 ×ˢ Icc 0 (2 * π)) (annulus_cc c r0 r1)

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
⊢ MapsTo (fun x => circleMap c x.1 x.2) (Icc r0 r1 ×ˢ Icc 0 (2 * π)) (annulus_cc c r0 r1)
Tactic:
intro x xs
State after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : x ∈ Icc r0 r1 ×ˢ Icc 0 (2 * π)
⊢ (fun x => circleMap c x.1 x.2) x ∈ annulus_cc c r0 r1

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : x ∈ Icc r0 r1 ×ˢ Icc 0 (2 * π)
⊢ (fun x => circleMap c x.1 x.2) x ∈ annulus_cc c r0 r1
Tactic:
simp only [Icc_prod_Icc, mem_Icc, Prod.le_def] at xs
State after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : (r0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ r1 ∧ x.2 ≤ 2 * π
⊢ (fun x => circleMap c x.1 x.2) x ∈ annulus_cc c r0 r1

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : (r0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ r1 ∧ x.2 ≤ 2 * π
⊢ (fun x => circleMap c x.1 x.2) x ∈ annulus_cc c r0 r1
Tactic:
have x0 : 0 ≤ x.1 := by linarith
State after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : (r0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ r1 ∧ x.2 ≤ 2 * π
x0 : 0 ≤ x.1
⊢ (fun x => circleMap c x.1 x.2) x ∈ annulus_cc c r0 r1

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : (r0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ r1 ∧ x.2 ≤ 2 * π
x0 : 0 ≤ x.1
⊢ (fun x => circleMap c x.1 x.2) x ∈ annulus_cc c r0 r1
Tactic:
simp only [circleMap, annulus_cc, mem_diff, Metric.mem_closedBall, dist_self_add_left,
  norm_mul, Complex.norm_eq_abs, Complex.abs_ofReal, abs_of_nonneg x0,
  Complex.abs_exp_ofReal_mul_I, mul_one, xs.2.1, Metric.mem_ball, not_lt, xs.1.1, and_self]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r0 r1 : ℝ
fc : ContinuousOn f (annulus_cc c r0 r1)
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : (r0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ r1 ∧ x.2 ≤ 2 * π
⊢ 0 ≤ x.1
Tactic:
linarith
State after:
no goals