-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
theorem Integrable.norm_integral_condKernel {f : α × Ω → E} (hf_int : Integrable f ρ) :
    Integrable (fun x ↦ ‖∫ y, f (x, y) ∂ρ.condKernel x‖) ρ.fst

Proof state:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ ‖‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖‖ ≤ ‖∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x‖

Tactic:
rw [norm_norm]

Result:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖ ≤ ‖∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x‖

Proof state:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖ ≤ ‖∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x‖

Tactic:
refine (norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg ?_).symm

Result:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ 0 ≤ ∫ (a : Ω), ‖f (x, a)‖ ∂ρ.condKernel x

Proof state:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖) ρ.fst

Tactic:
refine hf_int.integral_norm_condKernel.mono hf_int.1.integral_condKernel.norm ?_

Result:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, ‖‖∫ (y : Ω), f (a, y) ∂ρ.condKernel a‖‖ ≤ ‖∫ (y : Ω), ‖f (a, y)‖ ∂ρ.condKernel a‖

Proof state:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ 0 ≤ ∫ (a : Ω), ‖f (x, a)‖ ∂ρ.condKernel x

Tactic:
exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun y ↦ norm_nonneg _)

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, ‖‖∫ (y : Ω), f (a, y) ∂ρ.condKernel a‖‖ ≤ ‖∫ (y : Ω), ‖f (a, y)‖ ∂ρ.condKernel a‖

Tactic:
refine Filter.Eventually.of_forall fun x ↦ ?_

Result:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ ‖‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖‖ ≤ ‖∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x‖