OAI/MathematicalPhysics/Transonic.lean

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

Relativistic transonic profiles for the septic wave equation

The global profile construction follows Buckmaster and Chen, and the phase identities follow Shao, Wei, and Zhang. These profiles provide the relativistic profile input in Real-valued blowup for the defocusing septic wave equation by OpenAI.

This file declares nothing itself. It gathers the 7 imports below, so a file that imports it gets all of them.

Imports