mis intégrable avec la multiplication des fonctions

J'essaie de prouver ce lemme:mis intégrable avec la multiplication des fonctions

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)"

mais je ne pouvais pas. Je l'ai vu qu'il est prouvé pour l'addition et la soustraction:

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)

ou même pour la multiplication scalaire mais pas pour deux multiplication des fonctions?

Source

2016-09-27 O.J

Le problème est que ce n'est tout simplement pas vrai. La fonction f(x) = 1/sqrt(x) est intégrable sur l'ensemble (0; 1], et l'intégrale a la valeur 2. Son carré f(x)² = 1/x d'autre part n'est pas intégrable sur l'ensemble (0; 1.) L'intégrale diverge

Source

2016-09-27 11:26:02

Merci Manuel , mais dans le cas si nous avons ce lemme simple 'lemma mult: corrections fg ::" real ⇒ réel " suppose" set_integrable MA f "" set_integrable MA g " montre" (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) "' 'sans hypothèse ou comme ci-dessus (multiplication par deux fonctions) Je crois que cela ne peut pas être prouvé –

Ce lemme n'est pas vrai non plus. 'f' est intégrable,' f^2' ne doit pas nécessairement être intégrable, et alors certaines des intégrales se produisent g dans votre objectif sera indéfini. Qu'essayez-vous réellement de prouver? C'est à dire. De quoi as-tu besoin pour ce lemma? –

En fait, j'ai besoin de prouver l'inégalité intégrale de Schwarz pour les réels. Qui est comme ci-dessous: 'lemme schwaz_ineq: corrections M fg corrige :: "réel ⇒ réel" suppose "⋀x x ∈ A." "set_integrable MA f" "set_integrable MA g" indique" (LINT x: A | M. Fx * gx) ≤ sqrt (LINT x: A | M (fx)^2) * sqrt (LINT x: A | M (gx)^2) "'. Donc, cela revient à la nécessité de deux fonctions de multiplication. –

mis intégrable avec la multiplication des fonctions

Répondre

Questions connexes