α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂Measure.prod μ ν
⊢ (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
have A : (∫⁻ z, f z ∂μ.prod ν) = ∫⁻ z, hf.mk f z ∂μ.prod ν := lintegral_congr_ae hf.ae_eq_mk
α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂Measure.prod μ ν
B : (∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) = ∫⁻ (x : α), ∫⁻ (y : β), AEMeasurable.mk f hf (x, y) ∂ν ∂μ
⊢ (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂Measure.prod μ ν
⊢ (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
have B : (∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ) = ∫⁻ x, ∫⁻ y, hf.mk f (x, y) ∂ν ∂μ := by
  apply lintegral_congr_ae
  filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk]with _ ha using lintegral_congr_ae ha
no goals
α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂Measure.prod μ ν
B : (∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) = ∫⁻ (x : α), ∫⁻ (y : β), AEMeasurable.mk f hf (x, y) ∂ν ∂μ
⊢ (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
rw [A, B, lintegral_prod_of_measurable _ hf.measurable_mk]
case h
α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂Measure.prod μ ν
⊢ (fun a => ∫⁻ (y : β), f (a, y) ∂ν) =ᶠ[ae μ] fun a => ∫⁻ (y : β), AEMeasurable.mk f hf (a, y) ∂ν
α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂Measure.prod μ ν
⊢ (∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) = ∫⁻ (x : α), ∫⁻ (y : β), AEMeasurable.mk f hf (x, y) ∂ν ∂μ
apply lintegral_congr_ae
no goals
case h
α : Type u_1
α' : Type ?u.5363970
β : Type u_2
β' : Type ?u.5363976
γ : Type ?u.5363979
E : Type ?u.5363982
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f
A : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂Measure.prod μ ν
⊢ (fun a => ∫⁻ (y : β), f (a, y) ∂ν) =ᶠ[ae μ] fun a => ∫⁻ (y : β), AEMeasurable.mk f hf (a, y) ∂ν
filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk]with _ ha using lintegral_congr_ae ha