gesetzt integrierbar mit Funktionen Multiplikation

Ich versuche, dieses Lemma zu beweisen:gesetzt integrierbar mit Funktionen Multiplikation

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

und

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

aber ich konnte nicht. Ich habe gesehen, dass es für die Addition und Subtraktion ist bewiesen:

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)

oder sogar für Skalarmultiplikation aber nicht für zwei Funktionen Multiplikation?

Quelle

2016-09-27 O.J

Das Problem ist, dass es ganz einfach nicht wahr ist. Die Funktion f(x) = 1/sqrt(x) ist am Satz (0; 1) integrierbar, das Integral hat den Wert 2. Sein Quadrat f(x)² = 1/x ist dagegen nicht integrierbar (0; 1). Das Integral divergiert.

Quelle

2016-09-27 11:26:02

Danke Manuel , aber was, wenn wir dieses einfache Lemma haben 'Lemma mult: behebt fg :: "real ⇒ real" setzt voraus "set_integrable MA f" "set_integrable MA g" zeigt "(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) "" ohne Annahme oder Beweis wie oben (Multiplikation mit zwei Funktionen) I gess, dass dies nicht beweisen kann. –

Dieses Lemma ist auch nicht wahr. Wie ich oben sagte, wenn "f" ist integrierbar, "f^2" muss nicht notwendigerweise integrierbar sein, und dann treten einige der Integrale auf g in Ihrem Ziel wird undefiniert sein. Was willst du * eigentlich * beweisen? I.e. Wozu brauchst du dieses Lemma? –

Eigentlich muss ich die Schwarz-Integral-Ungleichung für Real beweisen. Welches als Gebrüll ist: 'Lemma schwaz_ineq: Fixes M Fixes fg :: "real ⇒ real" geht davon aus "⋀x x ∈ A." "set_integrable MA f" "set_integrable MA g" zeigt" (LINT x: A | M. fx * gx) ≤ sqrt (LINT x: A | M. (Fx)^2) * sqrt (LINT x: A | M. (Gx)^2) ". Also kommt es auf die Notwendigkeit der Multiplikation zweier Funktionen an. –

gesetzt integrierbar mit Funktionen Multiplikation

Antwort

Verwandte Themen