내가이 보조 정리를 증명하기 위해 노력하고있어 기능 곱셈

과 적분 설정 :내가이 보조 정리를 증명하기 위해 노력하고있어 기능 곱셈

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)

또는 스칼라 곱셈하지만 :이 덧셈과 뺄셈에 대한 입증되는 것을 나는 보았다?

출처

2016-09-27 O.J

문제는 매우 간단합니다. 함수 f(x) = 1/sqrt(x)은 집합 (0; 1)에 적분 가능하고 값 2를가집니다. 반면에 f(x)² = 1/x은 집합 (0; 1)에 적분되지 않습니다.

출처

2016-09-27 11:26:02

감사 마누엘 그러나 우리가이 간단한 보조 정리'lemma mult를 갖는다면 어떤 경우에 : fg :: "real ⇒ real"을 수정 함 "set_integrable MA f" "set_integrable MA g" 은 "(LINT x : A | (fx * gx)) + (fx * gx) + (fx * gx) + (fx * gx) LINT x : A | M (gx)^2) ""위의 가정이나 증명 (두 함수의 곱셈)이 없으면 증명할 수 없습니다. –

이 보조 정리는 참이 아닙니다. 'f'는 적분 가능하고,'f^2'는 반드시 적분 될 필요는 없으며, 적분의 일부가 발생합니다 당신의 목표에있는 g는 정의되지 않을 것입니다. 실제로 * 당신이 * 증명하려고 노력하고 있습니까? 나는. 이 보조 정리를 왜 필요로합니까? –

사실, 나는 슈왈츠 적분 불평등을 증명해야한다. 어느만큼 노호이다'표제어 schwaz_ineq : 수정 해결되는 FG을 M : "실제 리얼 ⇒" 는 ". ⋀x X ∈ A" "set_integrable MA의 F ''set_integrable MA의 g ' 쇼"(LINT의 X를 가정 A | M, fx * gx) ≤ sqrt (LINT x : A | M. (fx)^2) * sqrt (LINT x : A | M. (gx)^2) ". 따라서 이것은 두 개의 곱셈 곱셈에 대한 필요성에 달려 있습니다. –

내가이 보조 정리를 증명하기 위해 노력하고있어 기능 곱셈

답변

관련 문제