[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (id ω, id ω)) μ)
[PROOFSTEP]
rw [← aestronglyMeasurable_comp_snd_map_prod_mk_iff (measurable_id'' hm)] at hf 
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (id ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (id ω, id ω)) μ)
[PROOFSTEP]
simp_rw [id.def] at hf ⊢
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (ω, ω)) μ)
[PROOFSTEP]
exact hf
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable f
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
rw [← integrable_comp_snd_map_prod_mk_iff (measurable_id'' hm)] at hf 
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable fun x => f x.snd
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
simp_rw [id.def] at hf ⊢
[GOAL]
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable fun x => f x.snd
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
exact hf
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁴ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝³ : PolishSpace Ω
inst✝² : BorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
ω : Ω
⊢ ↑(condexpKernel μ m) ω = ↑(condDistrib id id μ) (id ω)
[PROOFSTEP]
simp_rw [condexpKernel, kernel.comap_apply]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁴ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝³ : PolishSpace Ω
inst✝² : BorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ IsMarkovKernel (condexpKernel μ m)
[PROOFSTEP]
simp only [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁴ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝³ : PolishSpace Ω
inst✝² : BorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ IsMarkovKernel (kernel.comap (condDistrib id id μ) id (_ : Measurable id))
[PROOFSTEP]
infer_instance
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ↑↑(↑(condexpKernel μ m) ω) s
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ↑↑(↑(condDistrib id id μ) (id ω)) s
[PROOFSTEP]
refine Measurable.mono ?_ (inf_le_left : m ⊓ mΩ ≤ m) le_rfl
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ↑↑(↑(condDistrib id id μ) (id ω)) s
[PROOFSTEP]
convert measurable_condDistrib (μ := μ) hs
[GOAL]
case h.e'_3
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ m ⊓ mΩ = MeasurableSpace.comap id (m ⊓ mΩ)
[PROOFSTEP]
rw [MeasurableSpace.comap_id]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω) μ
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id ω)) μ
[PROOFSTEP]
exact
  AEStronglyMeasurable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf.comp_snd_map_prod_id inf_le_right)
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω) μ
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) μ
[PROOFSTEP]
have h :=
  aestronglyMeasurable'_integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
h :
  AEStronglyMeasurable' (MeasurableSpace.comap id (m ⊓ mΩ))
    (fun a => ∫ (y : Ω), f (id a, y).snd ∂↑(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) μ
[PROOFSTEP]
rw [MeasurableSpace.comap_id] at h 
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : AEStronglyMeasurable f μ
h : AEStronglyMeasurable' (m ⊓ mΩ) (fun a => ∫ (y : Ω), f (id a, y).snd ∂↑(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) μ
[PROOFSTEP]
exact AEStronglyMeasurable'.mono h inf_le_left
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f
[PROOFSTEP]
exact
  Integrable.condDistrib_ae (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), ‖f y‖ ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), ‖f y‖ ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω
[PROOFSTEP]
exact
  Integrable.integral_norm_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ‖∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω‖
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ‖∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω‖
[PROOFSTEP]
exact
  Integrable.norm_integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ Integrable fun ω => ∫ (y : Ω), f y ∂↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω
[PROOFSTEP]
exact
  Integrable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Integrable fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)
[PROOFSTEP]
rw [condexpKernel]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
s : Set Ω
hs : MeasurableSet s
⊢ Integrable fun ω => ENNReal.toReal (↑↑(↑(kernel.comap (condDistrib id id μ) id (_ : Measurable id)) ω) s)
[PROOFSTEP]
exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
have h := condDistrib_ae_eq_condexp (μ := μ) (measurable_id'' (inf_le_right : m ⊓ mΩ ≤ mΩ)) measurable_id hs
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h :
  (fun a => ENNReal.toReal (↑↑(↑(condDistrib id id μ) (id a)) s)) =ᵐ[μ]
    μ[indicator (id ⁻¹' s) fun ω => 1|MeasurableSpace.comap id (m ⊓ mΩ)]
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
simp only [id_eq, ge_iff_le, MeasurableSpace.comap_id, preimage_id_eq] at h 
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : (fun a => ENNReal.toReal (↑↑(↑(condDistrib id id μ) a) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : (fun a => ENNReal.toReal (↑↑(↑(condDistrib id id μ) a) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condDistrib id id μ) (id ω)) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m ⊓ mΩ]
[PROOFSTEP]
exact h
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ μ[indicator s fun ω => 1|m ⊓ mΩ] =ᵐ[μ] μ[indicator s fun ω => 1|m]
[PROOFSTEP]
rw [inf_of_le_left hm]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[Measure.trim μ hm] μ[indicator s fun ω => 1|m]
[PROOFSTEP]
rw [ae_eq_trim_iff hm _ stronglyMeasurable_condexp]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)) =ᵐ[μ] μ[indicator s fun ω => 1|m]
[PROOFSTEP]
exact condexpKernel_ae_eq_condexp hm hs
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ StronglyMeasurable fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)
[PROOFSTEP]
refine Measurable.stronglyMeasurable ?_
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁵ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure Ω
inst✝¹ inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ Measurable fun ω => ENNReal.toReal (↑↑(↑(condexpKernel μ m) ω) s)
[PROOFSTEP]
exact @Measurable.ennreal_toReal _ m _ (measurable_condexpKernel hs)
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
have hX : @Measurable Ω Ω mΩ (m ⊓ mΩ) id := measurable_id.mono le_rfl (inf_le_right : m ⊓ mΩ ≤ mΩ)
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
hX : Measurable id
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condexpKernel μ m) ω
[PROOFSTEP]
simp_rw [condexpKernel_apply_eq_condDistrib]
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
hX : Measurable id
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id ω)
[PROOFSTEP]
have h := condexp_ae_eq_integral_condDistrib_id hX hf_int
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf_int : Integrable f
hX : Measurable id
h : μ[f|MeasurableSpace.comap id (m ⊓ mΩ)] =ᵐ[μ] fun a => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id a)
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂↑(condDistrib id id μ) (id ω)
[PROOFSTEP]
simpa only [MeasurableSpace.comap_id, id_eq] using h
[GOAL]
Ω : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace Ω
m mΩ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f
⊢ μ[f|m ⊓ mΩ] =ᵐ[μ] μ[f|m]
[PROOFSTEP]
rw [inf_of_le_left hm]
