集積與功能倍增

我試圖證明這個引理：集積與功能倍增

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

Thanks Manuel ，但如果我們有這個簡單的引理'引理mult：修復fg ::「真⇒真實的」假設「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）「'？沒有假設或證明像上面那樣（兩個函數相乘）我不能證明這個引理 –

正如我上面所說的，如果'f'是可積的，'f^2'不一定是可積的，然後一些積分出現在克在你的目標將是未定義的。你究竟在做什麼*試圖證明什麼？即你需要什麼這個引理？ –

其實，我需要證明施瓦茨積分不等式的真實性。這是波紋管：'引理schwaz_ineq：修復中號修復FG :: 「真實⇒真正的」假定「⋀xX∈A。」「set_integrable MA F」「set_integrable MA克」顯示「（LINT X：（LINX x：A | M（fx）^ 2）* sqrt（LINT x：A | M。（gx）^ 2）「'。所以這歸結爲需要兩個函數相乘。 –

集積與功能倍增

回答

相關問題