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!