setToFun_mono_left' — Mathlib

English

If T ≤ T' pointwise for all s and x, then setToFun μ T hT f ≤ setToFun μ T' hT' f for any integrable f.

Русский

Если T(s,x) ≤ T'(s,x) для всех s, x, то setToFun μ T hT f ≤ setToFun μ T' hT' f для интегрируемого f.

LaTeX

$$$\forall s,x,\; T(s,x) ≤ T'(s,x) \Rightarrow setToFun(\mu, T) h_T f ≤ setToFun(\mu, T') h_{T'} f$$$

Lean4

theorem setToFun_mono_left' {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x) (f : α → E) :
    setToFun μ T hT f ≤ setToFun μ T' hT' f :=
  by
  by_cases hf : Integrable f μ
  · simp_rw [setToFun_eq _ hf]; exact L1.setToL1_mono_left' hT hT' hTT' _
  · simp_rw [setToFun_undef _ hf, le_rfl]

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