internlm/Lean-Github huggingface dataset:
Theorem: invert_toReal
Proof state before:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal x.toReal
Tactic:
refine (ENNReal.ofReal_toReal ?_).symm
Proof state after:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x ≠ ⊤
Theorem: invert_toReal
Proof state before:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x ≠ ⊤
Tactic:
contrapose yp
Proof state after:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : ¬x ≠ ⊤
⊢ ¬y > 0
Theorem: invert_toReal
Proof state before:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : ¬x ≠ ⊤
⊢ ¬y > 0
Tactic:
simp only [ne_eq, not_not] at yp
Proof state after:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : x = ⊤
⊢ ¬y > 0
Theorem: invert_toReal
Proof state before:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : x = ⊤
⊢ ¬y > 0
Tactic:
simp only [yp, ENNReal.top_toReal] at h
Proof state after:
x : ENNReal
y : ℝ
yp : x = ⊤
h : 0 = y
⊢ ¬y > 0
Theorem: invert_toReal
Proof state before:
x : ENNReal
y : ℝ
yp : x = ⊤
h : 0 = y
⊢ ¬y > 0
Tactic:
simp only [← h, lt_self_iff_false, not_false_eq_true]
Proof state after:
no goals
Theorem: fubini_annulus
Proof 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
Proof 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)
Theorem: fubini_annulus
Proof 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 _]
Proof 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)
Theorem: fubini_annulus
Proof 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
Proof 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)
Theorem: fubini_annulus
Proof 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]
Proof 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)
Theorem: fubini_annulus
Proof 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
Proof 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)
Theorem: fubini_annulus
Proof 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)]
Proof 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)
Theorem: fubini_annulus
Proof 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
Proof 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)
Theorem: fubini_annulus
Proof 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]
Proof 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)
Theorem: fubini_annulus
Proof 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]
Proof 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)
Theorem: fubini_annulus
Proof 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]
Proof 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)
Theorem: fubini_annulus
Proof 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)]
Proof 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)
Theorem: fubini_annulus
Proof 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]
Proof 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)
Theorem: fubini_annulus
Proof 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
Proof 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)
Theorem: fubini_annulus
Proof 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]
Proof 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)
Theorem: fubini_annulus
Proof 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]
Proof 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)
Theorem: fubini_annulus
Proof 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)
Proof state after:
no goals
Theorem: fubini_annulus
Proof 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
Proof 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)
Theorem: fubini_annulus
Proof 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)]
Proof state after:
no goals
Theorem: fubini_annulus
Proof 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
Proof 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 * π))
Theorem: fubini_annulus
Proof 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
Proof state after:
no goals
Theorem: fubini_annulus
Proof 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
Proof 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 * π))
Theorem: fubini_annulus
Proof 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
Proof 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)
Theorem: fubini_annulus
Proof 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
Proof 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
Theorem: fubini_annulus
Proof 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
Proof 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
Theorem: fubini_annulus
Proof 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
Proof 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
Theorem: fubini_annulus
Proof 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]
Proof state after:
no goals
Theorem: fubini_annulus
Proof 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
Proof state after:
no goals
Theorem: fubini_ball
Proof 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
Proof 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)
Theorem: fubini_ball
Proof 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]
Proof 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)
Theorem: fubini_ball
Proof 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
Proof 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)