非负区间积分

Question

我正在寻找在区间积分中的引理状态，如果函数为非负或等于零，则积分也为非负或等于零。我在其他积分理论中看到过这个属性但在区间积分中没有看到。我试过这个引理：

引理 m4: 固定一个 b M 假定 "interval_lebesgue_integrable M a b (λx. f x)" “⋀x.0 ≤ f x” “⋯t.set_integrableM(einterval a b)(λx.f x)” “(⋯ a b. a≥0 ∧ a ≤ b )” 显示“(LINT t=a..b|M.f x) ≥0”

但是当我尝试使用 "quickcheck" 时，我收到了这条错误消息：对于 default_type Enum.finite_1 的实例化： Enum.finite_1 被替换为变量 'a 没有排序 {ord,banach,second_countable_topology} 对于 default_type Enum.finite_2 的实例化： Enum.finite_2 被替换为变量 'a 没有排序 {ord,banach,second_countable_topology} 对于 default_type Enum.finite_3 的实例化： Enum.finite_3 被替换为变量 'a 没有排序 {ord,banach,second_countable_topology}

我认为问题是 {ord} 没有包含在定义中的区间积分值中。

Answer 1

您不能指望 Quickcheck 能够处理包含积分的命题。 Quickcheck 需要能够为命题中涉及的所有内容生成可执行代码，并且没有用于集成的代码方程式，而且也不太可能编写任何代码。

至于你的引理，证明它只是展开定义并将相应的引理应用于“常规”勒贝格积分的问题。

lemma m4: 
  fixes a b :: ereal and f :: "real ⇒ real"
  assumes "interval_lebesgue_integrable M a b (λx. f x)" "a ≤ b" "⋀x. x ∈ {a<..<b} ⟹ 0 ≤ f x" 
  shows   "(LINT x=a..b|M. f x) ≥ 0"
  using assms unfolding interval_lebesgue_integral_def
  by (auto intro!: integral_nonneg_AE simp: indicator_def einterval_def)

（您给出的命题中有一些错误；我想这就是您真正想要的那种定理）

非负区间积分

Nonnegative Interval Integration

isabelle