Generalizing the Gagliardo-Nirenberg Inequality

Stream: mathlib4

[Joakim Björnander]

Hello everyone!

I'm currently working on a formalization of the full general Gagliardo–Nirenberg (interpolation) inequality in Lean.

https://en.wikipedia.org/wiki/Gagliardo%E2%80%93Nirenberg_interpolation_inequality#Statement_of_the_inequality

Theorem:
For any smooth function $u : \mathbb{R}^n \to \mathbb{R}$ with compact support, and for parameters $j, m, n, p, q, r, \alpha$ satisfying the dimensional scaling relation:

$\frac{1}{p} - \frac{j}{n} = \alpha \left( \frac{1}{r} - \frac{m}{n} \right) + (1 - \alpha)\frac{1}{q}$,

the following bound holds:

$\|D^j u\|_{L^p(\mathbb{R}^n)} \le C \|D^m u\|_{L^r(\mathbb{R}^n)}^a \|u\|_{L^q(\mathbb{R}^n)}^{1-a}$ 

Lean boilerplate:

-- The dimensional scaling relation (admissibility condition on exponents)
  def GNNormalizationRelation (j m n θ p q r : ℝ) : Prop :=
    1 / p = j / n + θ * (1 / r - m / n) + (1 - θ) / q

  -- Full validity: scaling relation + θ ∈ [j/m, 1] + exclusion of the exceptional endpoint
  -- (θ = 1 is excluded when 1 < r and m - j - n/r ∈ ℕ, where W^{k,r} ↪ BMO not L^∞)
  def GNValidExponents (j m n : ℕ) (p q r : ℝ≥0∞) (θ : ℝ) : Prop :=
    GNNormalizationRelation j m n θ p.toReal q.toReal r.toReal ∧
    (j : ℝ) / m ≤ θ ∧ θ ≤ 1 ∧
    ¬(1 < r ∧ (∃ k : ℕ, (k : ℝ) = m - j - n / r.toReal) ∧ θ = 1)

  -- The Lp norm of the k-th Fréchet derivative (via iteratedFDeriv)
  def TotalFDerivNorm (u : EuclideanSpace ℝ (Fin d) → ℝ) (k : ℕ) (p : ℝ≥0∞)
      (μ : Measure _ := volume) : ℝ≥0∞ :=
    eLpNorm (fun x => ‖iteratedFDeriv ℝ k u x‖) p μ

  -- The theorem statement (on ℝⁿ, smooth compactly supported functions)
  theorem gagliardo_nirenberg_general
      (j m d : ℕ) (p q r : ℝ≥0∞) (θ : ℝ) :
      ∀ u : EuclideanSpace ℝ (Fin d) → ℝ,
        ContDiff ℝ ⊤ u → HasCompactSupport u →
        GNValidExponents j m d p q r θ →
        ∃ C : ℝ, 0 ≤ C ∧
          TotalFDerivNorm u j p ≤
            ENNReal.ofReal C *
              (TotalFDerivNorm u m r) ^ θ *
              (eLpNorm u q volume) ^ (1 - θ) := by
    sorry -- work in progress

Relationship to Mathlib:

Mathlib currently contains an elegant implementation of the $j=0, m=1$ case (the Gagliardo–Nirenberg–Sobolev inequality) in Analysis.FunctionalSpaces.SobolevInequality. I am extending this to the full $(j, m)$ matrix. My strategy follows the double-induction approach from Fiorenza, Formica, Roskovec, and Soudský (2021), adapted to fit Mathlib's coordinate-free architecture. 

Formalization Strategy:

The proof is built on a hierarchy of lemmas designed to isolate the analytic difficulties from the combinatorial ones:

1. Coordinate-free Architecture: Using iteratedFDeriv and operator norms as the primary representation. This avoids the combinatorial explosion of multi-indices during the induction steps.
2. The 1D Base Case $(j=0, m=1)$: Proving the inequality on $\mathbb{R}$ using the Fundamental Theorem of Calculus and Hölder's inequality.
3. The $n$-Dimensional Lift: Using the existing Mathlib GNS proof (Doorn–Macbeth, eLpNorm_le_eLpNorm_fderiv_of_eq) as the seed, which handles the Loomis–Whitney iterated integration via the lmarginal construction.

4. Induction "Ladders":

   • $m$-Step: Combining a $(1,2)$ integration-by-parts estimate with the existing $(1,m)$ estimate to obtain $(1, m+1)$.
   • $j$-Step: Using the chain rule to show that validity for $(j, m)$ implies validity for $(j+1, m+1)$.

5. Scaling Principle: Using a dilation argument $u_\lambda(x) = u(\lambda x)$ to prove that the additive correction term vanishes on $\mathbb{R}^n$, recovering the pure multiplicative inequality.

Downstream Special Cases:
This formalization unifies many foundational PDE inequalities as special cases:

Sobolev Embedding: $W^{m,r} \hookrightarrow L^p$ appears as the non-critical $\alpha=1$ endpoint (subject to the exceptional case condition encoded in GNValidExponents).
Nash's Inequality: $j=0, p=2, m=1, r=2, q=1 \implies \alpha = \frac{n}{n+2}$
Ladyzhenskaya's Inequality: $n=2, j=0, p=4, m=1, r=2, q=2 \implies \alpha = 1/2$

Advice on Submission:
This project is becoming substantial. I would appreciate advice on how to best structure the files and PRs for Mathlib.

[Michael Rothgang]

Hi! Do you have a repository with your code somewhere already --- i.e., are you planning on doing this or, or have do done a lot of this already?

[Michael Rothgang]

Your message reads like it was written with substantial LLM input. Is this true/does the same hold for your Lean code? (It is quite common here to see new Lean users generating lots of code with an LLM that does not do what they think it does. That's obviously not a nice scenario.)

[Michael Rothgang]

To be clear: using an LLM is not banned per se --- but if you do it, please tell us - so we can help you in the most useful way. (Humans and LLMs make different errors, for example.)

[Joakim Björnander]

Hi, it is definitely LLM-assisted, you could say. I do not have it in a public repo yet, it really not at that stage yet. The only part that's fully finished is the double induction steps. It also need some cleaning up and improved structure. But will push it to GitHub as soon as I'm ready to show something :)

[Michael Rothgang]

Joakim Björnander said:

Advice on Submission:
This project is becoming substantial. I would appreciate advice on how to best structure the files and PRs for Mathlib.

This is very general question, so it's hard to give a useful answer. Can you be a more specific --- what have you done/what do you want to know? You will get much more helpful answers this way.

[Joakim Björnander]

Michael Rothgang said:

Joakim Björnander said:

Advice on Submission:
This project is becoming substantial. I would appreciate advice on how to best structure the files and PRs for Mathlib.

This is very general question, so it's hard to give a useful answer. Can you be a more specific --- what have you done/what do you want to know? You will get much more helpful answers this way.

For example: Are many small PRs preferred to a large PR with 10 files and 15 theorems and 40 lemmas?

[Michael Rothgang]

I would say

• try to make somewhat focused PRs. one PR doing five things are once is harder to review. don't mix large mechanical renames with moving code and adding new lemmas, etc.
• as a new user, aim for smaller PRs: perhaps 100 to 200 lines is a good ballpark
• you can open a big PR for the whole branch (this can be helpful to provide overall context) --- but expect the reviewing work to happen in smaller units

[Kevin Buzzard]

I think it is also worth saying that recently there have been many people saying "I have an AI-assisted development of theory X and want to get it into mathlib" and I think that so far 0 of these developments have ever actually made it over the line, because the quality of AI-written code is so poor compared to the code quality required by the mathlib maintainers. The user gets feedback, typically of the form "these proofs are 5x longer than the proof an expert would write, and there are way too many definitions, and some lemmas should be inlined, so right now this PR is completely unmergeable; please fix". And then what happens typically is that the user is completely unable to fix this problem because neither they nor the machine they use is able to fix up the code so that it is at the required standard. So I would think hard before sinking too much time into this.

[Kevin Buzzard]

What seems to me to be happening is that in the past, people who were able to get this kind of theorem over the line had already been forced to basically become an expert at writing mathlib-standard Lean code, because AI was useless and the learning all had to be done by the human. But now it has become much easier to get LLM-assistance to get stylistically poor but sorry-free code over the line, written by human-machine combos which have not gone through that learning curve (because the machine can't learn and the human hasn't learnt because the machine did all the hard work). The problem is that such code is not really acceptable for mathlib and is better off simply living in downstream repos.

This is why it's so important to see a preliminary version of your code. If it's a write-off as far as mathlib is concerned then the sooner you learn this the better. But if it's great, then great! Michael's comments above all apply.

[Joakim Björnander]

That's totally fair!

[Joakim Björnander]

In this case I have studied the proof structure from Fiorenza, Formica, Roskovec, and Soudský (2021). The first (that I know of) formal proof of the theorem.

I have then written an implementation-plan and for each small step I utilize an LLM to help out with the implementation.

[Kevin Buzzard]

Right, and what I'm flagging is that the code might be really horrible from an elegance perspective and thus utterly unsuitable for mathlib, and furthermore it might be the case that neither you nor your machine will be able to do anything about this because whilst there is clear competence in your system, there might be very little true lean expertise, which is what you need for mathlib-level code. But I can't say for sure until we see the code. I'm just warning you of a possible outcome.

[Kevin Buzzard]

And unfortunately the past few months on this zulip has given us example after example of this phenomenon. Probably eventually the machines will start writing expert-level code rather than "it compiles" code, but right now there is little evidence of this.

[Joakim Björnander]

Thanks for the advice