[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁷ : TopologicalSpace Ω
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : PolishSpace Ω
inst✝⁴ : BorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
inst✝ : MeasurableSpace β
⊢ IsMarkovKernel (condDistrib Y X μ)
[PROOFSTEP]
rw [condDistrib]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁷ : TopologicalSpace Ω
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : PolishSpace Ω
inst✝⁴ : BorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
inst✝ : MeasurableSpace β
⊢ IsMarkovKernel (Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ ((∀ᵐ (a : β) ∂Measure.map X μ, Integrable fun ω => f (a, ω)) ∧
      Integrable fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂↑(condDistrib Y X μ) a) ↔
    Integrable f
[PROOFSTEP]
rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prod_mk₀ hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂↑(condDistrib Y X μ) x) (Measure.map X μ)
[PROOFSTEP]
rw [← Measure.fst_map_prod_mk₀ hY, condDistrib]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂↑(Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ)) x)
    (Measure.fst (Measure.map (fun a => (X a, Y a)) μ))
[PROOFSTEP]
exact hf.integral_condKernel
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ Integrable fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)
[PROOFSTEP]
refine' integrable_toReal_of_lintegral_ne_top _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ AEMeasurable fun a => ↑↑(↑(condDistrib Y X μ) (X a)) s
[PROOFSTEP]
exact Measurable.comp_aemeasurable (kernel.measurable_coe _ hs) hX
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ↑↑(↑(condDistrib Y X μ) (X x)) s ∂μ ≠ ⊤
[PROOFSTEP]
refine' ne_of_lt _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ↑↑(↑(condDistrib Y X μ) (X x)) s ∂μ < ⊤
[PROOFSTEP]
calc
  ∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
  _ = μ univ := lintegral_one
  _ < ∞ := measure_lt_top _ _
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ ∀ᵐ (b : β) ∂Measure.map X μ, Integrable fun ω => f (b, ω)
[PROOFSTEP]
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ ∀ᵐ (b : β) ∂Measure.fst (Measure.map (fun a => (X a, Y a)) μ), Integrable fun ω => f (b, ω)
[PROOFSTEP]
exact hf_int.condKernel_ae
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂↑(condDistrib Y X μ) x
[PROOFSTEP]
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂↑(Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ)) x
[PROOFSTEP]
exact hf_int.integral_norm_condKernel
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ‖∫ (y : Ω), f (x, y) ∂↑(condDistrib Y X μ) x‖
[PROOFSTEP]
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ‖∫ (y : Ω), f (x, y) ∂↑(Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ)) x‖
[PROOFSTEP]
exact hf_int.norm_integral_condKernel
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (X ⁻¹' t ∩ Y ⁻¹' s)
[PROOFSTEP]
conv_lhs => arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ
[PROOFSTEP]
arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ
[PROOFSTEP]
arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ
[PROOFSTEP]
arg 2
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| fun a => ↑↑(↑(condDistrib Y X μ) (X a)) s
[PROOFSTEP]
change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
⊢ lintegral (Measure.restrict μ (X ⁻¹' t)) ((fun a => ↑↑(↑(condDistrib Y X μ) a) s) ∘ X) = ↑↑μ (X ⁻¹' t ∩ Y ⁻¹' s)
[PROOFSTEP]
rw [lintegral_comp (kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht, ←
  Measure.fst_map_prod_mk₀ hY, set_lintegral_condKernel_eq_measure_prod _ ht hs,
  Measure.map_apply_of_aemeasurable (hX.aemeasurable.prod_mk hY) (ht.prod hs), mk_preimage_prod]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (t ∩ Y ⁻¹' s)
[PROOFSTEP]
obtain ⟨t', ht', rfl⟩ := ht
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
t' : Set β
ht' : MeasurableSet t'
⊢ ∫⁻ (a : α) in X ⁻¹' t', ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (X ⁻¹' t' ∩ Y ⁻¹' s)
[PROOFSTEP]
rw [set_lintegral_preimage_condDistrib hX hY hs ht']
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ (fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)) =ᵐ[μ]
    μ[indicator (Y ⁻¹' s) fun ω => 1|MeasurableSpace.comap X mβ]
[PROOFSTEP]
refine' ae_eq_condexp_of_forall_set_integral_eq hX.comap_le _ _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ Integrable (indicator (Y ⁻¹' s) fun ω => 1)
[PROOFSTEP]
exact (integrable_const _).indicator (hY hs)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → ↑↑μ s_1 < ⊤ → IntegrableOn (fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)) s_1
[PROOFSTEP]
exact fun t _ _ => (integrable_toReal_condDistrib hX.aemeasurable hs).integrableOn
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ →
        ∫ (x : α) in s_1, ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X x)) s) ∂μ =
          ∫ (x : α) in s_1, indicator (Y ⁻¹' s) (fun ω => 1) x ∂μ
[PROOFSTEP]
intro t ht _
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in t, ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X x)) s) ∂μ =
    ∫ (x : α) in t, indicator (Y ⁻¹' s) (fun ω => 1) x ∂μ
[PROOFSTEP]
rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
    (eventually_of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
  integral_indicator_const _ (hY hs), Measure.restrict_apply (hY hs), smul_eq_mul, mul_one, inter_comm,
  set_lintegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ AEStronglyMeasurable' (MeasurableSpace.comap X mβ) (fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)) μ
[PROOFSTEP]
refine' (Measurable.stronglyMeasurable _).aeStronglyMeasurable'
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ Measurable fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)
[PROOFSTEP]
exact @Measurable.ennreal_toReal _ (mβ.comap X) _ (measurable_condDistrib hs)
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
⊢ μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)
[PROOFSTEP]
have hf_int' : Integrable (fun a => f (X a, Y a)) μ :=
  (integrable_map_measure hf_int.1 (hX.aemeasurable.prod_mk hY)).mp hf_int
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
⊢ μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)
[PROOFSTEP]
refine' (ae_eq_condexp_of_forall_set_integral_eq hX.comap_le hf_int' (fun s _ _ => _) _ _).symm
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s✝ : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ IntegrableOn (fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)) s
[PROOFSTEP]
exact (hf_int.integral_condDistrib hX.aemeasurable hY).integrableOn
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s < ⊤ → ∫ (x : α) in s, ∫ (y : Ω), f (X x, y) ∂↑(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in s, f (X x, Y x) ∂μ
[PROOFSTEP]
rintro s ⟨t, ht, rfl⟩ _
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (x : α) in X ⁻¹' t, ∫ (y : Ω), f (X x, y) ∂↑(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in X ⁻¹' t, f (X x, Y x) ∂μ
[PROOFSTEP]
change ∫ a in X ⁻¹' t, ((fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x') ∘ X) a ∂μ = ∫ a in X ⁻¹' t, f (X a, Y a) ∂μ
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (a : α) in X ⁻¹' t, ((fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x') ∘ X) a ∂μ =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (a : α) in X ⁻¹' t, ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a) ∂μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
[PROOFSTEP]
rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')]
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂↑(condDistrib Y X μ) y ∂Measure.map X (Measure.restrict μ (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x')
    (Measure.map X (Measure.restrict μ (X ⁻¹' t)))
[PROOFSTEP]
swap
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x')
    (Measure.map X (Measure.restrict μ (X ⁻¹' t)))
[PROOFSTEP]
rw [← Measure.restrict_map hX ht]
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x') (Measure.restrict (Measure.map X μ) t)
[PROOFSTEP]
exact (hf_int.1.integral_condDistrib_map hY).restrict
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂↑(condDistrib Y X μ) y ∂Measure.map X (Measure.restrict μ (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
[PROOFSTEP]
rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prod_mk₀ hY, condDistrib,
  set_integral_condKernel_univ_right ht hf_int.integrableOn,
  set_integral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prod_mk hY), mk_preimage_prod, preimage_univ,
  inter_univ]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
⊢ AEStronglyMeasurable' (MeasurableSpace.comap X mβ) (fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)) μ
[PROOFSTEP]
exact aestronglyMeasurable'_integral_condDistrib hX.aemeasurable hY hf_int.1
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int : Integrable fun a => f (X a, Y a)
⊢ Integrable f
[PROOFSTEP]
rwa [integrable_map_measure hf (hX.aemeasurable.prod_mk hY)]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf : StronglyMeasurable f
hf_int : Integrable fun a => f (X a, Y a)
⊢ Integrable f
[PROOFSTEP]
rwa [integrable_map_measure hf.aestronglyMeasurable (hX.aemeasurable.prod_mk hY)]
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
[PROOFSTEP]
refine' ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, _⟩
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ (fun x => f x.snd) =ᵐ[Measure.map (fun ω => (X ω, ω)) μ] fun x => AEStronglyMeasurable.mk f hf x.snd
[PROOFSTEP]
suffices h : Measure.QuasiMeasurePreserving Prod.snd (μ.map fun ω => (X ω, ω)) μ
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
h : Measure.QuasiMeasurePreserving Prod.snd
⊢ (fun x => f x.snd) =ᵐ[Measure.map (fun ω => (X ω, ω)) μ] fun x => AEStronglyMeasurable.mk f hf x.snd
[PROOFSTEP]
exact Measure.QuasiMeasurePreserving.ae_eq h hf.ae_eq_mk
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ Measure.QuasiMeasurePreserving Prod.snd
[PROOFSTEP]
refine' ⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => _⟩
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑(Measure.map Prod.snd (Measure.map (fun ω => (X ω, ω)) μ)) s = 0
[PROOFSTEP]
rw [Measure.map_apply _ hs]
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ Measurable Prod.snd
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ Measurable Prod.snd
[PROOFSTEP]
exact measurable_snd
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
by_cases hX : AEMeasurable X μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
rw [Measure.map_apply_of_aemeasurable]
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ ↑↑μ ((fun ω => (X ω, ω)) ⁻¹' (Prod.snd ⁻¹' s)) = 0
[PROOFSTEP]
rw [← univ_prod, mk_preimage_prod, preimage_univ, univ_inter, preimage_id']
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ ↑↑μ s = 0
[PROOFSTEP]
exact hμs
[GOAL]
case pos.hf
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ AEMeasurable fun ω => (X ω, ω)
[PROOFSTEP]
exact hX.prod_mk aemeasurable_id
[GOAL]
case pos.hs
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ MeasurableSet (Prod.snd ⁻¹' s)
[PROOFSTEP]
exact measurable_snd hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : ¬AEMeasurable X
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
rw [Measure.map_of_not_aemeasurable]
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : ¬AEMeasurable X
⊢ ↑↑0 (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : ¬AEMeasurable X
⊢ ¬AEMeasurable fun ω => (X ω, ω)
[PROOFSTEP]
contrapose! hX
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable fun ω => (X ω, ω)
⊢ AEMeasurable X
[PROOFSTEP]
exact measurable_fst.comp_aemeasurable hX
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
by_cases hX : AEMeasurable X μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
have hf := hf_int.1.comp_snd_map_prod_mk X (mΩ := mΩ) (mβ := mβ)
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
refine' ⟨hf, _⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ HasFiniteIntegral fun x => f x.snd
[PROOFSTEP]
rw [HasFiniteIntegral, lintegral_map' hf.ennnorm (hX.prod_mk aemeasurable_id)]
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ↑‖f (X a, a).snd‖₊ ∂μ < ⊤
[PROOFSTEP]
exact hf_int.2
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : ¬AEMeasurable X
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
rw [Measure.map_of_not_aemeasurable]
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : ¬AEMeasurable X
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : ¬AEMeasurable X
⊢ ¬AEMeasurable fun ω => (X ω, ω)
[PROOFSTEP]
contrapose! hX
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable fun ω => (X ω, ω)
⊢ AEMeasurable X
[PROOFSTEP]
exact measurable_fst.comp_aemeasurable hX
