набор интегрируемых с функцией умножения

Я пытаюсь доказать эту лемму:

  lemma set_integral_mult:
  fixes f g :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "set_integrable M A (λx. f x)"  "set_integrable M A (λx. g x)"
    shows "set_integrable M A (λx. f x * g x)"

и

  lemma set_integral_mult1:
  fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "set_integrable M A (λx. f x)"  
    shows "set_integrable M A (λx. f x * f x)"

но я не мог. Я видел, что это доказано для сложения и вычитания:

  lemma set_integral_add [simp, intro]:
  fixes f g :: "_ ⇒ _ :: {banach, second_countable_topology}"
  assumes "set_integrable M A f" "set_integrable M A g"
  shows "set_integrable M A (λx. f x + g x)"
    and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
  using assms by (simp_all add: scaleR_add_right)

  lemma set_integral_diff [simp, intro]:
  assumes "set_integrable M A f" "set_integrable M A g"
  shows "set_integrable M A (λx. f x - g x)" and "LINT x:A|M. f x - g x =
    (LINT x:A|M. f x) - (LINT x:A|M. g x)"
  using assms by (simp_all add: scaleR_diff_right)

или даже для скалярного умножения, но не для умножения двух функций?


theorem-proving isabelle
person O.J    schedule 27.09.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Проблема в том, что это совсем не так. Функция f(x) = 1 / sqrt(x) интегрируема на множестве (0; 1], а интеграл имеет значение 2. С другой стороны, ее квадрат f(x)² = 1 / x не интегрируем на множестве (0; 1]. Интеграл расходится.

person Manuel Eberl    schedule 27.09.2016
comment
Спасибо, Мануэль, но что в случае, если у нас есть эта простая лемма `lemma mult: fixes fg :: real ⇒ real предполагает set_integrable MA f set_integrable MA g показывает (LINT x: A | M. ((Fx) ⇧2 + (fx * gx) + (gx) ⇧2)) = (LINT x: A | M. (fx) ^ 2) + (LINT x: A | M. (fx * gx)) + (LINT x: A | M. ( gx) ^ 2) `? без предположений или доказательств, как указано выше (умножение на две функции), я полагаю, что это не может доказать. - person O.J; 27.09.2016
comment
Эта лемма также неверна. Как я сказал выше, если f интегрируемый, f^2 не обязательно должен быть интегрируемым, и тогда некоторые из интегралов, встречающихся в вашей цели, будут неопределенными. Что вы на самом деле пытаетесь доказать? Т.е. зачем вам эта лемма? - person Manuel Eberl; 28.09.2016
comment
Собственно, мне нужно доказать интегральное неравенство Шварца для вещественных чисел. Как показано ниже: lemma schwaz_ineq: fixes M fixes f g :: "real ⇒ real" assumes "⋀x. x ∈ A" "set_integrable M A f " "set_integrable M A g " shows " (LINT x:A|M. f x * g x ) ≤ sqrt(LINT x:A|M. (f x)^2 ) * sqrt(LINT x:A|M. (g x)^2)" . Это сводится к необходимости умножения двух функций. - person O.J; 29.09.2016
comment
Вы не сможете ничего подобного доказать, потому что, если f^2 не интегрируется на A, то LINT x:A|M. (f x)^2 не определено в Isabelle. Вероятно, вы могли бы показать это для nn_integral, поскольку, если f интегрируется, а f^2 нет, это по существу означает, что f^2 измеримо, но его интеграл бесконечен. Тогда вам просто нужно будет различать регистр, интегрируются ли f^2 и g^2 или нет. В зависимости от вашей конечной цели, вероятно, проще просто предположить, что f^2 и g^2 интегрируемы, как это делают и некоторые учебники. - person Manuel Eberl; 29.09.2016
comment
Мануэль, большое спасибо за ваши объяснения. По сути, я доказал это, предположив, что f^2 и g^2 интегрируемы, но я хочу уменьшить количество предположений в моей основной теории, просто предполагая, что f и g интегрируемы. Однако, похоже, я не могу этого сделать. еще раз спасибо. - person O.J; 29.09.2016