α : Type u_2
α' : Type ?u.4449024
β : Type u_1
β' : Type ?u.4449030
γ : Type ?u.4449033
E : Type ?u.4449036
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : ↑↑(Measure.prod μ' ν') s = 0
⊢ ↑↑(Measure.prod μ ν) s = 0
α : Type u_2
α' : Type ?u.4449024
β : Type u_1
β' : Type ?u.4449030
γ : Type ?u.4449033
E : Type ?u.4449036
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
⊢ Measure.prod μ ν ≪ Measure.prod μ' ν'
refine' AbsolutelyContinuous.mk fun s hs h2s => _
α : Type u_2
α' : Type ?u.4449024
β : Type u_1
β' : Type ?u.4449030
γ : Type ?u.4449033
E : Type ?u.4449036
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (fun x => ↑↑ν' (Prod.mk x ⁻¹' s)) =ᶠ[ae μ'] 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
α : Type u_2
α' : Type ?u.4449024
β : Type u_1
β' : Type ?u.4449030
γ : Type ?u.4449033
E : Type ?u.4449036
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : ↑↑(Measure.prod μ' ν') s = 0
⊢ ↑↑(Measure.prod μ ν) s = 0
rw [measure_prod_null hs] at h2s ⊢
no goals
α : Type u_2
α' : Type ?u.4449024
β : Type u_1
β' : Type ?u.4449030
γ : Type ?u.4449033
E : Type ?u.4449036
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (fun x => ↑↑ν' (Prod.mk x ⁻¹' s)) =ᶠ[ae μ'] 0
⊢ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
exact (h2s.filter_mono h1.ae_le).mono fun _ h => h2 h