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.