| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Provers/Arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 2 kB |
|
Quellcode-Bibliothek holder_scaf.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Holder's Inequality % % Author: David Lester, Manchester University % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Version 1.0 12/3/10 Initial Version %------------------------------------------------------------------------------ holder_scaf[(IMPORTING measure_integration@subset_algebra_def, measure_integration@measure_def) T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S], p:{a:real | a > 1}, q:{a:posreal | 1/p + 1/a = 1}]: THEORY BEGIN IMPORTING p_integrable_def, young, % Proof only measure_integration@integral[T,S,mu] % Proof only f: VAR p_integrable[T,S,mu,p] g: VAR p_integrable[T,S,mu,q] holder_aux: LEMMA p_integrable?[T,S,mu,1](f*g) AND norm[T,S,mu,1](f*g) <= norm[T,S,mu,p](f) * norm[T,S,mu,q](g) holder_judge1: JUDGEMENT *(f,g) HAS_TYPE p_integrable[T,S,mu,1] holder_judge2: JUDGEMENT *(g,f) HAS_TYPE p_integrable[T,S,mu,1] holder_scaf: LEMMA norm[T,S,mu,1](f*g) <= norm[T,S,mu,p](f) * norm[T,S,mu,q](g) END holder_scaf ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28