integral_exp_pos — Mathlib

English

If F is integrable and f = exp(F) is integrable, then ∫ exp(F) > 0.

Русский

Если F интегрируем, а exp(F) интегрируем, то интеграл exp(F) положителен.

LaTeX

$$$0 < \\\\int a \\, e^{F(a)} \\, d\\\\mu$$$

Lean4

theorem integral_exp_pos {μ : Measure α} {f : α → ℝ} [hμ : NeZero μ] (hf : Integrable (fun x ↦ Real.exp (f x)) μ) :
    0 < ∫ x, Real.exp (f x) ∂μ :=
  by
  rw [integral_pos_iff_support_of_nonneg (fun x ↦ (Real.exp_pos _).le) hf]
  suffices (Function.support fun x ↦ Real.exp (f x)) = Set.univ by simp [this, hμ.out]
  ext1 x
  simp only [Function.mem_support, ne_eq, (Real.exp_pos _).ne', not_false_eq_true, Set.mem_univ]

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