integral_convexOn_of_integrand_ae

English

If the integrand f(x,a) is concave in a and integrable, then the integral is concave as a function of a.

Русский

Если f(x,a) выпукло по a в обратном смысле? — конкавно, то интеграл по a во всех переменных являетcя выпуклоопределяемой функцией.

LaTeX

$$$ConcaveOn( a \\mapsto ∫ f(x,a) dμ)$ under concavity of f in a and integrability.$$

Lean4

theorem integral_convexOn_of_integrand_ae {β : Type*} [AddCommMonoid β] [Module ℝ β] {f : α → β → E} {s : Set β}
    (hs : Convex ℝ s) (hf_conv : ∀ᵐ x ∂μ, ConvexOn ℝ s (f x)) (hf_int : ∀ a ∈ s, Integrable (f · a) μ) :
    ConvexOn ℝ s (fun b => ∫ x, f x b ∂μ) := by
  refine ⟨hs, ?_⟩
  intro a ha b hb p q hp hq hpq
  calc
    ∫ x, f x (p • a + q • b) ∂μ ≤ ∫ x, p • f x a + q • f x b ∂μ :=
      by
      refine integral_mono_ae ?lhs ?rhs ?ae_le
      case lhs =>
        refine hf_int _ ?_
        rw [convex_iff_add_mem] at hs
        exact hs ha hb hp hq hpq
      case rhs => fun_prop (disch := aesop)
      case ae_le =>
        filter_upwards [hf_conv] with x hx
        exact hx.2 ha hb hp hq hpq
    _ = ∫ x, p • f x a ∂μ + ∫ x, q • f x b ∂μ := by
      apply integral_add
      all_goals fun_prop (disch := aesop)
    _ = p • ∫ x, f x a ∂μ + q • ∫ x, f x b ∂μ := by simp [integral_smul]

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