💻 computer science

A Formalization of the Laplace Transform and Its Inversion in Lean 4

Dit artikel presenteert een Lean 4-formalisering van de Laplace-transformatie en de inversie ervan via een Bromwich-type stelling, waarbij de toepassing ervan op de harmonische oscillator wordt gedemonstreerd terwijl belangrijke analytische en formaliseringsuitdagingen worden geadresseerd.

Oorspronkelijke auteurs: Daniel Goldberg, Antoine Vinciguerra

Gepubliceerd 2026-08-10

📖 7 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Daniel Goldberg, Antoine Vinciguerra

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je een wereld voor waarin de chaotische, rommelige beweging van dingen die veranderen in de tijd—zoals een zwaaiende pendel, een trillende gitaarsnaar of een signaal dat door een draad reist—instantaan vertaald kan worden naar een schoon, statisch algebraïsch probleem. Dit is de magie van de Laplace-transformatie, een wiskundig hulpmiddel dat ingenieurs en wetenschappers al meer dan een eeuw gebruiken. Zie het als een universele vertaler die een verhaal vertaalt dat geschreven is in de taal van de "tijd" (waar dingen bewegen, versnellen en vertragen) naar een verhaal dat geschreven is in de taal van "complexe getallen" (waar diezelfde bewegingen eenvoudige vermenigvuldiging en deling worden).

Waarom is dit belangrijk? Omdat het oplossen van vergelijkingen over hoe dingen veranderen vaak ontzettend moeilijk is, alsof je probeert een knoop te ontwarren terwijl er aan wordt getrokken. Maar als je die knoop kunt vertalen naar een andere taal waar het er simpelweg uitziet als een rechte lijn, kun je het gemakkelijk oplossen en de oplossing vervolgens weer terugvertalen. Dit artikel gaat over het bouwen van een "bewijscontroleur" voor deze vertaler. De auteurs hebben niet alleen de regels opgeschreven; ze hebben een computerprogramma genaamd Lean 4 gebruikt om wiskundig stap voor stap te bewijzen dat de vertaler precies doet wat beloofd wordt, zelfs voor de lastigste delen van het proces. Ze wilden ervoor zorgen dat wanneer we deze krachtige instrumenten gebruiken om bruggen, circuits of controlesystemen te ontwerpen, de onderliggende wiskunde rotsvast is en vrij is van verborgen fouten.

De Digitale Bewijscontroleur

Stel je voor dat je een zeer strikte, zeer letterlijke robotvriend hebt die van wiskunde houdt maar een hekel heeft aan gokken. Je zegt tegen hem: "Hier is een formule die een golvende lijn in een vloeiende curve verandert," en hij vraagt: "Weet je het zeker? Wat als de lijn te veel golft? Wat als hij eeuwig doorgaat?" Dit artikel is het resultaat van twee onderzoekers, Daniel en Antoine, die hun robotvriend alles hebben geleerd wat hij moet weten over de Laplace-transformatie.

Ze hebben niet alleen een tekstboek geschreven; ze hebben een volledige, computer-geverifieerde bibliotheek gebouwd in Lean 4. Dit is een programmeertaal die specifiek is ontworpen voor het schrijven van wiskundige bewijzen die een computer op fouten kan controleren. Hun doel was om de Laplace-transformatie—een methode die functies van de tijd omzet in functies van complexe getallen—te nemen en te bewijzen dat elke regel werkt, van de basisdefinities tot het complexe "inversieproces" dat de oplossing weer terugvertaalt naar de tijd.

De Vertaler en de Magische Spiegel

De Laplace-transformatie is als een magische spiegel. Je plaatst een functie $f(t)$ (die beschrijft wat er in de loop van de tijd gebeurt) in de spiegel, en het reflecteert een nieuwe functie $(Lf)(s)$ (die hetzelfde beschrijft in een "frequentiewereld").

De Heenreis: Het artikel bewijst dat als je een functie hebt die zich netjes gedraagt (niet te snel naar oneindig explodeert), de spiegel werkt. Ze bewezen de regels voor hoe je eenvoudige zaken zoals constanten, machten van de tijd en zelfs sinusgolven vertaalt. Bijvoorbeeld, ze lieten zien dat de spiegel de afgeleide (de veranderingssnelheid) omzet in een eenvoudige vermenigvuldiging met een getal $s$ , minus een beginwaarde. Dit is het "geheime ingrediënt" dat het oplossen van differentiaalvergelijkingen zo makkelijk maakt.
De Terugreis (Inversie): De echte uitdaging is het terugkrijgen van het antwoord. Hoe kijk je naar de reflectie en weet je precies wat het oorspronkelijke object was? Dit wordt de inverse Laplace-transformatie genoemd. Het artikel bewijst een specifieke methode om dit te doen, bekend als de Bromwich-formule.

Waarom ze niet voor de "makkelijke" route kozen

Meestal bewijzen wiskundigen de inversieformule met een techniek die complexe contourintegratie wordt genoemd. Stel je voor dat je een lus rond een vorm op een kaart tekent en een speciale stelling gebruikt (de Residustelling) om de "schatten" binnenin te tellen. Het is een krachtig hulpmiddel, maar de auteurs ontdekten dat de bibliotheek van de computer nog niet genoeg van deze "kaarttekenende" hulpmiddelen ingebouwd had.

Daarom kozen ze een andere, meer fundamentele weg. In plaats van lussen te tekenen in het complexe vlak, behandelden ze het probleem als een real-world integratie over een rechte lijn. Ze braken het probleem af in kleinere, beheersbare stukken:

Afkapping (Truncation): Ze deden alsof de oneindige lijn slechts een kort, eindig segment was van $-T$ tot $T$ .
De Sinc-functie: Naarmate ze dit segment langer en langer maakten, ontstond er een specifiek patroon met een functie genaamd sinc (die eruitziet als een golf die steeds kleiner wordt).
Het Dirichlet-integraal: Ze vertrouwden op een beroemd, reeds bewezen feit over de oppervlakte onder deze sinc-golf (het Dirichlet-integraal) om aan te tonen dat wanneer het segment oneindig lang wordt, het resultaat de oorspronkelijke functie perfect reconstrueert.

Deze aanpak was moeilijker op te zetten, maar veiliger voor de computer om te verifiëren omdat het vertrouwde op reële calculus, waar de computer al erg goed in was.

De Test met de Zwaaiende Pendel

Om te bewijzen dat hun systeem echt werkt, controleerden ze niet alleen abstracte wiskunde; ze losten een klassiek natuurkundig probleem op: de harmonische oscillator. Dit is de wiskunde achter een zwaaiende pendel of een springende veer.

De Opstelling: Ze definieerden een veer die vanuit rust begint maar een snelle duw krijgt, beschreven door de vergelijking $y''(t) + \omega^2 y(t) = 0$ .
De Vertaling: Ze voerden deze vergelijking in hun computer-geverifieerde Laplace-vertaler.
Het Resultaat: De computer slaagde erin de rommelige differentiaalvergelijking om te zetten in een eenvoudige algebraïsche vergelijking: $(s^2 + \omega^2)Y(s) = \omega$ .
De Oplossing: Het oplossen voor $Y(s)$ gaf hen $\frac{\omega}{s^2 + \omega^2}$ .
De Verificatie: De computer controleerde vervolgens zijn eigen bibliotheek en bevestigde dat dit specifieke resultaat exact de Laplace-transformatie is van $\sin(\omega t)$ .

Dit was een groot succes. Het betekende dat de computer niet alleen het antwoord berekende; het bewees dat het antwoord inderdaad een sinusgolf is, wat overeenkomt met wat menselijke natuurkundigen al eeuwenlang weten, maar dan met een niveau van zekerheid waar geen ruimte is voor menselijke fouten.

De Strikte Regels van het Spel

Het artikel is ook een les in hoe voorzichtig je moet zijn wanneer je stopt met gokken en begint met bewijzen. De auteurs wijzen op verschillende "valstrikken" die in tekstboeken vaak worden weggestopt:

Oneindigheid is lastig: Je kunt niet zomaar aannemen dat een integraal naar oneindig gaat. Het bewijs moest expliciet vermelden dat de functie snel genoeg moet afnemen zodat de "staart" van de integraal verdwijnt.
De Randgevallen: Bij het uitvoeren van de wiskunde zijn er specifieke punten (zoals tijd $t=0$ ) waar de regels veranderen. De computer dwong hen om precies te zijn over waar de functie gedefinieerd en continu is.
Volgorde Wisselen: Bij het bewijs van de inversie moesten ze de volgorde van twee integralen omdraaien. In informele wiskunde doe je dit misschien gewoon. In hun formele bewijs moesten ze rigoureus bewijzen dat de "oppervlakte" onder het gecombineerde oppervlak eindig was voordat ze de volgorde mochten wisselen.

De Kern van het Verhaal

Dit artikel is een mijlpaal in de formele verificatie. Het ontdekt geen nieuwe natuurwet of vindt een nieuw type golf uit. In plaats daarvan bouwt het een fort van zekerheid rond een instrument dat al breed wordt gebruikt. Door de Laplace-transformatie en de inversie ervan te vertalen naar een taal die een computer kan controleren, hebben de auteurs een referenstandaard gecreëerd.

Ze bewezen dat de "magische spiegel" werkt, mits je de strikte regels volgt over hoe de functie zich gedraagt bij oneindig en bij het begin. Ze lieten zien dat de weg naar het antwoord een zorgvuldige, stapsgewijze logica vereist in plaats van afkortingen. Voor iedereen die de volgende generatie software bouwt die op deze wiskundige instrumenten vertrouwt, zorgt dit werk ervoor dat de fundering niet alleen sterk is, maar ook onbreekbaar. Het voorbeeld van de harmonische oscillator dient als de definitieve goedkeuring: de computer is het eens met de mens, en voor het eerst heeft de computer het bewijs officieel ondertekend.

Technische Samenvatting: Een Formalisering van de Laplace-transformatie en de Inversie ervan in Lean 4

Probleemstelling
Het artikel behandelt de formalisering van de Laplace-transformatie en de inversie daarvan binnen de Lean 4 theorem prover, waarbij specifiek gebruik wordt gemaakt van de mathlib bibliotheek. Hoewel de Laplace-transformatie een standaardinstrument is in de toegepaste wiskunde voor het omzetten van lineaire differentiaalvergelijkingen naar algebraïsche vergelijkingen, vormt de rigoureuze formalisering ervan aanzienlijke uitdagingen. Deze omvatten het hanteren van complex-waardige functies, het beheren van onbeperkte integralen (limieten van afgeknotte integralen versus Lebesgue-integralen) en het bewijzen van de inversiestelling zonder te vertrouwen op complexe contourintegratie en residustheorema's, die nog niet voldoende ontwikkeld zijn in de huidige Lean 4 bibliotheek.

Methodologie
De auteurs hanteren een meettheoretische benadering die geworteld is in het Bochner-integraalraamwerk dat beschikbaar is in mathlib. De ontwikkeling verloopt via verschillende cruciale methodologische keuzes:

Abstracte Kernconstructie: De transformatie wordt eerst gedefinieerd in een algemene setting over een voltooide genormeerde algebra $E$ met behulp van een kern $e^{-L(e,p)}$ . Deze abstracte laag isoleert de algebraïsche eigenschappen van de exponentiële kern van specifieke meettheoretische keuzes.
Specialisatie naar Reële Functies: De constructie wordt gespecialiseerd naar complex-waardige functies op de reële lijn. De auteurs maken gebruik van twee representaties:
- Een mapped-measure benadering, waarbij de Lebesgue-maat op $[0, \infty)$ wordt voorgeschoven naar de reële as binnen $\mathbb{C}$ , gebruikt primair voor de inversiestelling.
- Een direct set-integral benadering over $(0, \infty)$ , gebruikt voor operationele regels en het voorbeeld van de harmonische oscillator.
Hantering van Onbeperkte Integralen: De formalisering behandelt de Laplace-transformatie expliciet als een limiet van afgeknotte integralen (over $(0, T]$ ) in plaats van een directe onbeperkte integraalnotatie. Dit onderscheid is cruciaal voor de correcte toepassing van de Dominated Convergence Theorem binnen het Lean-raamwerk.
Reële Variabele Inversie: In plaats van de standaard complex-analytische bewijsvoering met contourdeformatie en het Residustheorema, bewijzen de auteurs de inversiestelling met behulp van reële variabele integratie. Door de Bromwich-contour te parametriseren als $s = \gamma + ir$ $s = γ + i r$ , wordt de integraal over de verticale lijn omgezet in een integraal over $r \in \mathbb{R}$ $r \in R$ . Het bewijs steunt vervolgens op:
- Fubini's Theorema om de volgorde van integratie te wisselen.
- Het Dirichlet-integraal (geformaliseerd in een aparte module [9]) om de oscillerende kern $\frac{\sin(T(t-a))}{t-a}$ te behandelen.
- Integratie door delen en de eigenschappen van de primitieve van het Dirichlet-integraal om puntgewijze convergentie naar de oorspronkelijke functie aan te tonen.

Kernbijdragen
Het artikel presenteert vier hoofd bijdragen aan de formele wiskundige gemeenschap:

Gegeneraliseerde Transformatie Formalisering: Een definitie van de Laplace-kern en transformatie op een voltooide genormeerde algebra, inclus inclusief bewijzen voor scalaire en additieve wetten.
Operationele Regels en Convergentie: Een formalisering van de transformatie als een Bochner-integraal over de positieve halve lijn. De auteurs bewijzen de convergentie van afgeknotte transformaties en stellen gesloten vorm formules vast voor constanten, machten, exponenten, afgeleiden (inclusief geïtereerde afgeleiden), trigonometrische functies (sinus en cosinus) en schaling. Deze bewijzen worden uitgevoerd onder expliciete integrabiliteits- en verval-aannames.
Bromwich-type Inversiestelling: Een formeel bewijs dat de inverse Laplace-transformatie een differentieerbare functie $f(t)$ herstelt op elk punt in een voorgeschreven verzameling $S \subset (0, \infty)$ . Dit bewijs maakt gebruik van het geformaliseerde Dirichlet-integraal en vermijdt complexe contourintegratie door te vertrouwen op reële parameter-integralen en de dominated convergence theorem.
Toepassing op de Harmonische Oscillator: Een volledige formele afleiding van de oplossing in het Laplace-domein voor de harmonische oscillatorvergelijking $y''(t) + \omega^2 y(t) = 0$ met beginvoorwaarden $y(0)=0, y'(0)=\omega$ . De stelling identificeert de transformatie van de oplossing met $\frac{\omega}{s^2 + \omega^2}$ , waarbij alle analytische hypothesen (regulariteit, integrabiliteit, verval) die meestal in tekstboekafleidingen worden weggelaten, expliciet worden geverifieerd.

Resultaten
De formele ontwikkeling bestaat uit ongeveer 2.900 regels Lean-code verspreid over vier bronbestanden. Belangrijke resultaten zijn onder meer:

Theorem RealLaplaceTransformIs: Ontvouwt de abstracte constructie naar de bekende integraalvorm.
Theorem IsInverseLaplace: Stelt de puntgewijze convergentie van de inverse transformatie naar de oorspronkelijke functie $f(t)$ vast onder voorwaarden van continuïteit, differentieerbaarheid en de integrabiliteit van $f(t)e^{-\gamma t}$ en zijn afgeleide.
Theorem harmonic_oscillator_laplace_eq: Bewijst dat de Laplace-transformatie van een functie die voldoet aan de harmonische oscillatorvergelijking gelijk is aan de transformatie van $\sin(\omega t)$ .

Betekenis en Omvang
De auteurs positioneren dit werk als een fundamentele stap in de formalisering van de toegepaste analyse. De betekenis ligt in:

Het Overbruggen van de Kloof: Het bieden van een werkende inversiestelling in Lean 4 zonder te wachten op de ontwikkeling van een volledige complexe residutheorie.
Expliciete Hypothesen: De formalisering legt de analytische condities bloot (zoals randverval en de integrabiliteit van gewogen afgeleiden) die vaak impliciet zijn in klassieke behandelingen, wat een rigoureuze correctheid garandeert.
Modulaire Architectuur: De scheiding van de abstracte kern, de specialisatie naar de reële as en de toepassingvoorbeelden creëert een herbruikbare structuur voor toekomstige ontwikkelingen.

Het artikel concludeert door op te merken dat hoewel convolutie en andere operationele regels natuurlijke vervolgstappen zijn, deze zorgvuldige behandeling vereisen en niet in dit manuscript worden behandeld. Het werk wordt gepresenteerd als een specifieke formalisering van de voorwaartse transformatie, de inversiestelling en een canonieke toepassing, in plaats van een allesomvattende bibliotheek van alle eigenschappen van de Laplace-transformatie.