Formalizing some fluid PDE theory.

Stream: mathlib4

[Fan Zheng]

Is there any interest in the community in formalizing local/global wellposedness (or even blow-up) of the Euler equation? @Terence Tao

[Terence Tao]

My understanding is that even the Sobolev embedding theorem has not been formalized yet in Lean, so I would say that this is premature.

[Fan Zheng]

Well we could do it in the Hőlder space. It would sound a little bit weird if Lean has something as sophisticated as perfectoid spaces but not basic PDE theory.

[Fan Zheng]

As for Sobolev spaces, I do remember seeing Gagliardo-Nirenberg somewhere in mathlib.

[Patrick Massot]

https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.37

[Patrick Massot]

by @Floris van Doorn and @Heather Macbeth

[Fan Zheng]

So, I'm trying to get started with singular integrals. There are two places that seem to contain some theory of integrals: Analysis/BoxIntegral and MeasureTheory/Integral. Which one should I take as a starting point?

[Patrick Massot]

Did you read the integration chapter of #mil? It doesn’t contain much but it would answer that question and some others.

[Fan Zheng]

OK. Thanks for the pointer.

[Michael Rothgang]

The Sobolev embedding theorem is on my medium-term list of things to get to - but don't let that keep you from thinking about it!

[Anatole Dedecker]

Guess I'd better go back to formalizing distributions then!

[Michael Rothgang]

That would be very welcome. A student of @Floris van Doorn worked on this last spring, see https://github.com/fpvandoorn/BonnAnalysis/tree/master/BonnAnalysis/Distributions

[Terence Tao]

If you want to proceed just from Holder spaces then it might be possible to formalize Sections 4.1, 4.2, 4.5 of Bertozzi-Majda with current tools, but it might be a fairly large lift.

[Fan Zheng]

Terence Tao ha dicho:

If you want to proceed just from Holder spaces then it might be possible to formalize Sections 4.1, 4.2, 4.5 of Bertozzi-Majda with current tools, but it might be a fairly large lift.

OK, so at least the first theorem (existence of ODE) in Section 4.1 of Bertozzi-Majda is already here:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/ODE/PicardLindelof.lean
right? And for the rest of the proof, is it better to have an outline like this one:
https://imperialcollegelondon.github.io/FLT/blueprint/sect0001.html
If so, how can I make one?

[Fan Zheng]

@Kevin Buzzard How can I make a blueprint like this one:
https://imperialcollegelondon.github.io/FLT/blueprint/sect0001.html

[Ruben Van de Velde]

You can search for "lean blueprint"

[Kevin Buzzard]

If you're lucky enough to be me then you just wait for someone else to do it for you and never learn how. And then when it breaks you have to constantly ask for help :-/ There's some kind of moral there I think

[Chris Birkbeck]

A good place to start is by cloning this repo and following the instructions there: https://github.com/pitmonticone/LeanProject

[Fan Zheng]

@Ruben Van de Velde I'm at this step:
https://pygraphviz.github.io/documentation/stable/install.html
installing PyGraphviz,
but after inputting the command in the command line, it gives the following error message:
Collecting pygraphviz
Downloading pygraphviz-1.14.tar.gz (106 kB)
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 106.0/106.0 kB ? eta 0:00:00
Installing build dependencies ... done
Getting requirements to build wheel ... error
error: subprocess-exited-with-error

× Getting requirements to build wheel did not run successfully.
│ exit code: 1
╰─> [6 lines of output]
usage: _in_process.py [global_opts] cmd1 [cmd1_opts] [cmd2 [cmd2_opts] ...]
or: _in_process.py --help [cmd1 cmd2 ...]
or: _in_process.py --help-commands
or: _in_process.py cmd --help

  error: option -L not recognized
  [end of output]

note: This error originates from a subprocess, and is likely not a problem with pip.
error: subprocess-exited-with-error

× Getting requirements to build wheel did not run successfully.
│ exit code: 1
╰─> See above for output.

note: This error originates from a subprocess, and is likely not a problem with pip.

[notice] A new release of pip available: 22.3.1 -> 25.0.1
[notice] To update, run: python.exe -m pip install --upgrade pip

[Ruben Van de Velde]

I wonder if we could make lake exe setup-blueprint work in projects that depend on mathlib

[Kim Morrison]

Ideally this would even be in a separate project -- no need for the actual implementation to be in Mathlib. I wouldn't object to Mathlib itself "requiring" it, to make the exe available for everyone downstream.

[Ruben Van de Velde]

Yeah, "if they depend on mathlib", not "iff" :)

[Fan Zheng]

@Kim Morrison I installed the Lean project but when I issued the command leanblueprint pdf it says:
Sorry, but latexmk did not succeed for the following reason:

MiKTeX could not find the script engine 'perl' which is required to execute 'latexmk'.

Remedy:

Make sure 'perl' is installed on your system.

The log file hopefully contains the information to get MiKTeX going again:

C:\Users\Fan\AppData\Local\MiKTeX\miktex\log\latexmk.log

For more information, visit: https://miktex.org/kb/fix-script-engine-not-found
Command 'latexmk -output-directory=../print' returned non-zero exit status 1.

I installed perl and the same error remains.

[Fan Zheng]

Moroever, the webpage it generated says:
--- permalink: /404.html layout: default ---

404

Page not found :(

The requested page could not be found.

[Derek Rhodes]

@Fan Zheng, it sounds like perl is either not on your PATH, or not on a path that miktex uses. Someone over on stackoverflow encountered a similar error, and resolved it by installing a specific distribution of called strawberry perl, which sounds heavy handed to me. Have you tried checking to see if perl is on your PATH?

Another supporting clue (from 2017) regarding this issue, someone asks Is there anyway to configure MiKTeX so that it locates script engine perl.exe:

I found that the path of perl.exe must be in environment PATH. This is the only way I could make MiKTeX's latexmk.exe run.

[Fan Zheng]

I installed strawberry perl, but the error remains.

[Eric Wieser]

I'm not sure if leanblueprint is really supported on windows, but maybe @Patrick Massot knows otherwise

[Fan Zheng]

Also I don't see anything related to perl in my PATH.
On that matter, the one thing I noted strange is that when I installed strawberry perl, it defaulted the directory of installation to the root directory of C:, which is quite unusual. I didn't change that. Maybe that is the problem?

[Patrick Massot]

This latexmk issue has nothing to do with leanblueprint, it’s all about generating the pdf version.

[Patrick Massot]

But indeed the leanblueprint command line interface calls latexmk.