Theorem: MeasureTheory.setIntegral_integral_swap (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ ∫ (x : α) in s, ∫ (y : β) in t, f x y ∂ν ∂μ = ∫ (y : β) in t, ∫ (x : α) in s, f x y ∂μ ∂ν
Tactic:
apply integral_integral_swap
State after:
case hf
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ Integrable (Function.uncurry fun x y => f x y) ((μ.restrict s).prod (ν.restrict t))

State before:
case hf
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ Integrable (Function.uncurry fun x y => f x y) ((μ.restrict s).prod (ν.restrict t))
Tactic:
convert hf.integrable
State after:
case h.e'_6
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)

State before:
case h.e'_6
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
Tactic:
exact Measure.prod_restrict s t
State after:
no goals