norm_integral_condKernel — Mathlib

English

If f is integrable, then the norm of the inner integral is integrable over the base measure.

Русский

Если f интегрируема, то норма внутреннего интеграла по базовой мере интегрируема.

LaTeX

$$$\\mathrm{Integrable}\\left( x \\mapsto \\left\\| \\int_y f(x,y) \\partial(\\rho.condKernel x) \\right\\| \\right) \\rho.fst$$$

Lean4

theorem norm_integral_condKernel {f : α × Ω → E} (hf_int : Integrable f ρ) :
    Integrable (fun x ↦ ‖∫ y, f (x, y) ∂ρ.condKernel x‖) ρ.fst :=
  by
  refine hf_int.integral_norm_condKernel.mono hf_int.1.integral_condKernel.norm ?_
  refine Filter.Eventually.of_forall fun x ↦ ?_
  rw [norm_norm]
  refine (norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg ?_).symm
  exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun y ↦ norm_nonneg _)

Похожие утверждения