lintegral_nnnorm_condExpIndSMul_le

English

For hm ≤ m0, hs measurable, hμs ≠ ∞ and x ∈ G, the nonnegative Lintegral of the nn-norm of condExpIndSMul over t is bounded by μ(s ∩ t) times ‖x‖₊.

Русский

Для hm ≤ m0, hs измеримо, hμs ≠ ∞ и x ∈ G, линтеграл по t от нормы condExpIndSMul ограничен μ(s ∩ t)·‖x‖₊.

LaTeX

$$$\int^{∞}_{a\in t} \|\operatorname{condExpIndSMul} hm hs hμs x a\|_+ ∂μ ≤ μ(s \cap t) \cdot \|x\|_+$$$

Lean4

theorem lintegral_nnnorm_condExpIndSMul_le (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G)
    [SigmaFinite (μ.trim hm)] : ∫⁻ a, ‖condExpIndSMul hm hs hμs x a‖₊ ∂μ ≤ μ s * ‖x‖₊ :=
  by
  refine lintegral_le_of_forall_fin_meas_trim_le hm (μ s * ‖x‖₊) fun t ht hμt => ?_
  refine (setLIntegral_nnnorm_condExpIndSMul_le hm hs hμs x ht hμt).trans ?_
  gcongr
  apply Set.inter_subset_left

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