α : Type u_2
α' : Type ?u.4500248
β : Type u_4
β' : Type ?u.4500254
γ : Type u_3
E : Type ?u.4500260
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
δ : Type u_1
inst✝ : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
hfa : SigmaFinite (map f μa)
hgc : SigmaFinite (map g μc)
hf : Measurable f
hg : Measurable g
this : SigmaFinite μc
⊢ Measure.prod (map f μa) (map g μc) = map (Prod.map f g) (Measure.prod μa μc)
α : Type u_2
α' : Type ?u.4500248
β : Type u_4
β' : Type ?u.4500254
γ : Type u_3
E : Type ?u.4500260
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
δ : Type u_1
inst✝ : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
hfa : SigmaFinite (map f μa)
hgc : SigmaFinite (map g μc)
hf : Measurable f
hg : Measurable g
⊢ Measure.prod (map f μa) (map g μc) = map (Prod.map f g) (Measure.prod μa μc)
haveI := hgc.of_map μc hg.aemeasurable
α : Type u_2
α' : Type ?u.4500248
β : Type u_4
β' : Type ?u.4500254
γ : Type u_3
E : Type ?u.4500260
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
δ : Type u_1
inst✝ : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
hfa : SigmaFinite (map f μa)
hgc : SigmaFinite (map g μc)
hf : Measurable f
hg : Measurable g
this : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (Prod.map f g) (Measure.prod μa μc)) (s ×ˢ t) = ↑↑(map f μa) s * ↑↑(map g μc) t
α : Type u_2
α' : Type ?u.4500248
β : Type u_4
β' : Type ?u.4500254
γ : Type u_3
E : Type ?u.4500260
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
δ : Type u_1
inst✝ : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
hfa : SigmaFinite (map f μa)
hgc : SigmaFinite (map g μc)
hf : Measurable f
hg : Measurable g
this : SigmaFinite μc
⊢ Measure.prod (map f μa) (map g μc) = map (Prod.map f g) (Measure.prod μa μc)
refine' prod_eq fun s t hs ht => _
α : Type u_2
α' : Type ?u.4500248
β : Type u_4
β' : Type ?u.4500254
γ : Type u_3
E : Type ?u.4500260
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
δ : Type u_1
inst✝ : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
hfa : SigmaFinite (map f μa)
hgc : SigmaFinite (map g μc)
hf : Measurable f
hg : Measurable g
this : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(Measure.prod μa μc) (Prod.map f g ⁻¹' s ×ˢ t) = ↑↑μa (f ⁻¹' s) * ↑↑μc (g ⁻¹' t)
α : Type u_2
α' : Type ?u.4500248
β : Type u_4
β' : Type ?u.4500254
γ : Type u_3
E : Type ?u.4500260
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
δ : Type u_1
inst✝ : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
hfa : SigmaFinite (map f μa)
hgc : SigmaFinite (map g μc)
hf : Measurable f
hg : Measurable g
this : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (Prod.map f g) (Measure.prod μa μc)) (s ×ˢ t) = ↑↑(map f μa) s * ↑↑(map g μc) t
rw [map_apply (hf.prod_map hg) (hs.prod ht), map_apply hf hs, map_apply hg ht]
no goals
α : Type u_2
α' : Type ?u.4500248
β : Type u_4
β' : Type ?u.4500254
γ : Type u_3
E : Type ?u.4500260
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
δ : Type u_1
inst✝ : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
hfa : SigmaFinite (map f μa)
hgc : SigmaFinite (map g μc)
hf : Measurable f
hg : Measurable g
this : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(Measure.prod μa μc) (Prod.map f g ⁻¹' s ×ˢ t) = ↑↑μa (f ⁻¹' s) * ↑↑μc (g ⁻¹' t)
exact prod_prod (f ⁻¹' s) (g ⁻¹' t)