α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
⊢ map f (Measure.prod μ ν) ≪ τ
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
⊢ QuasiMeasurePreserving f
refine' ⟨hf, _⟩
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
s : Set γ
hs : MeasurableSet s
h2s : ↑↑τ s = 0
⊢ ↑↑(map f (Measure.prod μ ν)) s = 0
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
⊢ map f (Measure.prod μ ν) ≪ τ
refine' AbsolutelyContinuous.mk fun s hs h2s => _
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
s : Set γ
hs : MeasurableSet s
h2s : ↑↑τ s = 0
⊢ (∫⁻ (x : α), ↑↑ν (Prod.mk x ⁻¹' (f ⁻¹' s)) ∂μ) = 0
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
s : Set γ
hs : MeasurableSet s
h2s : ↑↑τ s = 0
⊢ ↑↑(map f (Measure.prod μ ν)) s = 0
rw [map_apply hf hs, prod_apply (hf hs)]
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
s : Set γ
hs : MeasurableSet s
h2s : ↑↑τ s = 0
⊢ (∫⁻ (x : α), ↑↑ν ((fun x_1 => f (x, x_1)) ⁻¹' s) ∂μ) = 0
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
s : Set γ
hs : MeasurableSet s
h2s : ↑↑τ s = 0
⊢ (∫⁻ (x : α), ↑↑ν (Prod.mk x ⁻¹' (f ⁻¹' s)) ∂μ) = 0
simp_rw [preimage_preimage]
no goals
α : Type u_1
α' : Type ?u.4534735
β : Type u_2
β' : Type ?u.4534741
γ : Type u_3
E : Type ?u.4534747
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ✝ : Measure γ
inst✝¹ : NormedAddCommGroup E
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝ : SigmaFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving fun y => f (x, y)
s : Set γ
hs : MeasurableSet s
h2s : ↑↑τ s = 0
⊢ (∫⁻ (x : α), ↑↑ν ((fun x_1 => f (x, x_1)) ⁻¹' s) ∂μ) = 0
rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero]