Moreira-2001 (generalization of Sard's theorem)

Stream: maths

[Yury G. Kudryashov]

I'm reading (and trying to formalize) Moreira's version of Sard's theorem, and I can't understand (at least) 1 step. In the proof of Theorem 2.1, page 152, case $k \ge 1$, when dealing with $A^*=\{x \in A \mid \exists g \colon U \xrightarrow{C^k} \mathbb R, g|_A \equiv 0, \exists v \in \mathbb R^{n - p}\times \{0\}, dg(x) \cdot v \ne 0\}$, he uses the implicit function theorem to find a $C^k$ smooth map $\psi\colon B\times V \xrightarrow{C^k} U$, $B \subset \mathbb R^{n - p - 1}$ (probably, with $\psi (x, y) = (\tilde\psi(x, y), y)$) such that its image covers a nhd of $x$ in $A$, then calls the inductive hypothesis. However, $\psi$ is a $C^k$ map, so there is no guarantee that $f \circ \psi$ will be a $C^{k + (\alpha)}$ smooth.

Is there a gap here, or am I missing something trivial?

[Sébastien Gouëzel]

Don't you just need to define $A^*=\{x \in A \mid \exists g \colon U \xrightarrow{C^{k+(\alpha)}} \mathbb R, g|_A \equiv 0, \exists v \in \mathbb R^{n - p}\times \{0\}, dg(x) \cdot v \ne 0\}$ to fix the argument?

[Sébastien Gouëzel]

(It means you would need an implicit function theorem in $C^{k+(\alpha)}$, but this should probably hold without difficulty).

[Sébastien Gouëzel]

By the way, I don't know if you've noticed that several lemmas of the paper are already in mathlib, as I've needed them for the proof of the change of variables formula. For instance, Theorem 3.3 is docs#MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero (well, Theorem 3.3 is just a little bit weaker than our result in mathlib, in fact :-), and the lemmas used in the proof in mathlib correspond more or less to what he uses in the paper.

[Yury G. Kudryashov]

Thanks! I should really learn not to post such questions after midnight. About Thm 3.3, I've noticed this, thanks!

[Yury G. Kudryashov]

@Sébastien Gouëzel Do you know what's the right generalization of Moreira's theorem to ContDiffOn (+some Holder condition) on a not necessarily open set?

[Yury G. Kudryashov]

Probably, assuming that the outer set U is UniqueDiffOn and using iteratedFDerivWithin everywhere will work (not 100% sure about the implicit function theorem in this case - can it lead to a non-UniqueDiffOn domain? - will think about it tomorrow after work)

[Yury G. Kudryashov]

But I see that the lemma you've linked above has even weaker assumptions.

[Yury G. Kudryashov]

Also, some steps rely on (local star?) convexity of U. Not sure if we can easily avoid it, since it's used with something like docs#domain_mvt

[Sébastien Gouëzel]

Instead of UniqueDiffOn, you could use an assumption like HasFTaylorSeriesUpToOn (and local Hölder conditions on the given k-th derivative), just like the above lemma uses HasFDerivWithinAt. But since you also need controls given by Taylor inequalities, local convexity seems necessary. So my guess it that "any point in U has a convex neighborhood with nonempty interior within U" is probably a good condition -- the nonempty interior implies unique differentiability, so no need to assume it separately. And since the proof is local, you might as well assume from the start that U is convex with nonempty interior (which would be enough for the application to manifolds with boundary or corners, for instance).

[Yury G. Kudryashov]

Thanks!

[Yury G. Kudryashov]

I have 2 new questions:

• is there a name for $C^{k + (\alpha)}$ as it is defined in the paper ($f\in C^k(U)$ with $D^kf(x) - D^kf(a) = O\left(\|x - a\|^\alpha\right)$ as $x \to a$ for all $a \in K$), or should I use something like ContDiffMoreiraHolderOn?
• is there a version of the inverse function theorem for a function defined on a convex set with nonempty interior, instead of a function defined in a nhd?

[Yury G. Kudryashov]

The second is needed to prove the main theorem for functions that are $C^{k+α}$ on a convex set.

[Yury G. Kudryashov]

An alternative way to move it to manifolds is to introduce a typeclass saying that the range of a model is an intersection of finitely many half-spaces (or a union of finitely many convex intrinsically open sets - both work for this case).

[Sébastien Gouëzel]

Yury G. Kudryashov said:

• is there a name for $C^{k + (\alpha)}$ as it is defined in the paper ($f\in C^k(U)$ with $D^kf(x) - D^kf(a) = O\left(\|x - a\|^\alpha\right)$ as $x \to a$ for all $a \in K$), or should I use something like ContDiffMoreiraHolderOn?

Not as far as I know, so your suggestion seems fine.

[Sébastien Gouëzel]

Yury G. Kudryashov said:

• is there a version of the inverse function theorem for a function defined on a convex set with nonempty interior, instead of a function defined in a nhd?

That depends on the precise version you want, but typically the answer is no. For instance, in the plane, consider a function defined on $\{x \ge 0\}$ that skews things a little bit to the right (like $(x, y) \mapsto (x + y^2, y)$). Then it maps the half-plane to itself, with a bijective differential at zero (the identity), but it is not locally surjective.

[Yury G. Kudryashov]

Then I'm going to aim for one of the typeclasses on the model I mentioned above.

[Yury G. Kudryashov]

Yet another option is to prove Whitney's extension theorem, but this is a separate project.

[Igor Khavkine]

Yury G. Kudryashov said:

• is there a name for $C^{k + (\alpha)}$ as it is defined in the paper ($f\in C^k(U)$ with $D^kf(x) - D^kf(a) = O\left(\|x - a\|^\alpha\right)$ as $x \to a$ for all $a \in K$), or should I use something like ContDiffMoreiraHolderOn?

Is this not just the definition of a function belonging to a Hölder space? I think I've seen this property referred to as "Hölder regular" or "Hölder differentiable". So even ContDiffHolderOn sounds alright.

[Yury G. Kudryashov]

No, the Holder condition is required only for $a \in K \subset U$, with constant and nhd depending on $a$.

[Yury G. Kudryashov]

I don't know if we'll ever need this difference in conditions, but I want to formalize the paper without losing generality.

[Yury G. Kudryashov]

If someone else is interested in collaborating on formalization of the Moreira/Sard theorem, then please contact me. I have a half-done blueprint that covers most (all?) of section 2, nothing from section 3 yet.

[Yury G. Kudryashov]

https://github.com/urkud/SardMoreira/blob/main/SardMoreira/MainTheorem.lean now contains

theorem hausdorffMeasure_sardMoreiraBound_image_null_of_finrank_le
    [MeasurableSpace F] [BorelSpace F]
    (hp_dom : p < dim E) (hk : k ≠ 0) {f : E → F} {s U : Set E}
    (hf : ContDiffMoreiraHolderOn k α f s U)
    (hs : ∀ x ∈ s, dim (LinearMap.range <| fderiv ℝ f x) ≤ p) :
    μH[sardMoreiraBound (dim E) k α p] (f '' s) = 0 := by

proved without sorrys.

[Sébastien Gouëzel]

(I just hope that sardMoreiraBound is the right bound :-)

[Yury G. Kudryashov]

It's defined in the same file,

noncomputable def sardMoreiraBound (n k : ℕ) (α : I) (p : ℕ) : ℝ≥0 :=
  p + (n - p) / (k + ⟨α, α.2.1⟩)

[Yury G. Kudryashov]

Last time I checked, it was the best available estimate, but it's possible I've missed some recent paper.

[Yury G. Kudryashov]

I've dumped some thoughts on upstreaming to https://github.com/urkud/SardMoreira/blob/8bd10dfe9de4739c7c947044992900ecb4edd1e7/README.md
It is not on main, because I don't want to cancel a CI run.

[Yury G. Kudryashov]

If you have better ideas on how to organize the process, I'm open to suggestions.

[Yury G. Kudryashov]

@Sébastien Gouëzel I've just sent Moreira an e-mail asking if he knows a nice way to apply his theorem to manifolds with boundaries.

[Alfredo Moreira-Rosa]

Weird feeling seeing my name on a thread. But that's not abour me :smile:

[Sébastien Gouëzel]

I think Whitney's extension is probably the way to go. I might have a try at it.

[Yury G. Kudryashov]

Do you know (a) what's the current best result about Whitney's extension; (b) what's the right way to formulate the corresponding differentiability notion with continuous multilinear forms?

[Yury G. Kudryashov]

If you don't have strong preferences, I would like to try it myself first.

[Yury G. Kudryashov]

I think that for Whitney differentiability, we should use formal series in the sense we use them for analytic functions, not formal Taylor series, then say that they satisfy the equalities we have for them in the analytic case, but with finite sums and +O(_).

[Sébastien Gouëzel]

Yes, I agree with all your comments. Whitney's paper is nice and the results there are pretty comprehensive, I'm not sure there's room for improvement. Wikipedia says that this is also explained in Hörmander, this is probably a good reference. For finer result, there is Fefferman's finitary version (https://annals.math.princeton.edu/wp-content/uploads/annals-v161-n1-p10.pdf) but I don't think they're worth pursuing for now.

[Sébastien Gouëzel]

And if you're willing to try it, I'm happy to let you!

[Yury G. Kudryashov]

What do you think about the following more direct approach to applying Sard's theorem to manifolds? We require that the model is an intersection of finitely many half spaces, then treat the result as a stratified union of manifolds without border.

[Sébastien Gouëzel]

I don't think it's a good idea: it would work in full generality with Whitney, so adding an artificial restriction doesn't feel mathliby. Also, the differential on the stratified components of the boundary doesn't coincide with the full differential, so this wouldn't give the same set of singular values if I understand correctly.

[Yury G. Kudryashov]

I should learn not to post when I'm tired/sleepy/...

[Yury G. Kudryashov]

I see that Whitney uses some very specific "bump" function which tends to infinity at the origin instead of being 1 in a nhd of the origin. Is it important?

[Sébastien Gouëzel]

I don't remember. Have you looked at Hörmander, or only at Whitney's original paper?

[Yury G. Kudryashov]

Only the original paper for now. I'll find a way to get Hormander's book later today.

[Yury G. Kudryashov]

I've started looking at the proof in Hörmander's book. It starts with a version of smooth bump functions with controlled derivatives. The proof in the book does not guarantee that the support is equal to the "outer" open set, see Theorem 1.4.1&1.4.2 there. What do you think is the best way to make it work with our setup?

[Yury G. Kudryashov]

@Sébastien Gouëzel :up:

[Sébastien Gouëzel]

I had a look at Hörmander, and I realize that the version he gives is not good enough (only for compact sets, finite differentiability, and does not guarantee that the function is analytic on the complement). So maybe it's a better idea to follow the original paper of Whitney.

In any case since it's supposed to be for a self-contained result I think you should first start with self-contained constructions (i.e., not trying too strongly to match them with existing objects in Mathlib) and once the proof is complete investigate if there can be synergies.

[Yury G. Kudryashov]

Thanks!

[Yury G. Kudryashov]

BTW, what do you think about this definition of $C^k$: https://projecteuclid.org/journalArticle/Download?urlId=10.36045%2Fbbms%2F1197908901 ? It looks very similar to Whitney differentiability (I haven't verified the details) and it gives a notion of $C^k$ that implies some nice properties even over fields of positive characteristic. Disclaimer: I first saw this a few days ago.

[Yury G. Kudryashov]

Next 2 PRs from this project: #33611 and #33582