lintegral_nnnorm_condExpL2_indicator_le

English

Another form of the bound on the L1-like integral of the norm for condExpL2 with indicator.

Русский

Еще одна форма предела интеграла нормы для condExpL2 индикатора.

LaTeX

$$setLIntegral_nnnorm_condExpL2_indicator_le (hm) (hs) (hμs) (x) (ht) (hμt)$$

Lean4

theorem lintegral_nnnorm_condExpL2_indicator_le (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E')
    [SigmaFinite (μ.trim hm)] : ∫⁻ a, ‖(condExpL2 E' 𝕜 hm (indicatorConstLp 2 hs hμs x) : α → E') a‖₊ ∂μ ≤ μ s * ‖x‖₊ :=
  by
  refine lintegral_le_of_forall_fin_meas_trim_le hm (μ s * ‖x‖₊) fun t ht hμt => ?_
  refine (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_
  gcongr
  apply Set.inter_subset_left

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