Skalarprodukt von Vektorräumen

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Skalarprodukt von Vektorräumen
Gibt es in smglom ein Skalarprodukt von Vektorräumen, bisher konnten wir keines finden und würden uns aus + und skalarmult sonst ein eigenes schreiben.


Gibt es glaub ich nicht - wird aber schwierig die zu definieren denke ich. Was euch natürlich nicht abhalten sollte, nur beruhigen falls ihr es nicht hinkriegen solltet :slight_smile:


Darf ich anmerken, dass das kein sonderlich hilfreicher Tipp ist :stuck_out_tongue:


Dennis und ich haben uns vor einer Stunde zufällig genau über Skalarprodukte und Hilberträume (HR) unterhalten.
Am einfachsten ist es, wenn du dich auf HRs X über R beschränkst. Dann ist dein Skalarprodukt eine binäre Funktion h: X → X → R und du kannst etwa die positive Definitheit \forall x. (x, x) >= 0 genau so definieren.

Wenn dein HR über C ist, dann typchecked „(x, x) >= 0“ (mit >= auf den reellen Zahlen) nicht mehr. Man möchte eigentlich so etwas wie „\vdash \forall x. (x, x) \in R“ schreiben könne, das ist aber laut Dennis in MMT aktuell nicht möglich. Der Grund ist, dass R und C Typen sind und Ausdrücke über Typen wie „\vdash (x, x) \in R“ nicht möglich sind.

Wenn du es noch allgemeiner haben willst: HR über einen Körper der Charakteristik 0, welcher einen vollständig geordnerten Teilkörper enthält und ferner auch bestimmte Eigenschaften erfüllt, sodass Komplexkonjugation übertragen werden kann. (Siehe auch die englische Wikipedia zu „Inner Product Spaces“, da steht das mit Charakteristik 0 und den anderen Dingen).

Spielst du hier auf das Standardskalarprodukt auf R^n an? Ich wusste gar nicht, dass smglom R^n enthält - außer man definiert sich das als n-maliger Product Space von R.
Dabei fällt mir ein: sind n-Tupel (in Abhängigkeit von n) aktuell formalisierbar? Es wäre ja nützlich, alle R^n und auch das Standardskalarprodukt parametrisiert in n definieren zu können.