feat(Geometry/Manifold): riemannian metrics exist

[idontgetoutmuch]

Using a partition of unity, we prove the existence of a smooth Riemannian metric.

The idea is that there are two equivalent ways of defining a bilinear positive definite form:

1. pull back the inner product on the model fiber F along the inverse trivialization;
2. push a pair of fiber vectors forward into F, then apply the inner product there.

Definition (1) makes smoothness straightforward: locally the form is smooth, provided the domain is taken small enough: the intersection of the trivialization's base set with the chart source. Global smoothness then follows from a partition of unity.

It is less clear (to me at least) how to get positive-definiteness from (1). This is what (2) is for: with vectors pushed forward into an inner product space, positivity, definiteness and symmetry are immediate. We prove the two definitions agree, transferring these properties back to (1).

One step remains. Mathlib's ContMDiffRiemannianMetric requires the the set where the form is less than 1 to be von Neumann bounded:

Let $E$ be a real vector bundle over a manifold $B$, with model fiber $F$, an inner product space; $E_b$ the fiber over $b \in B$ and $e_i : E_b \to F$ the fiberwise linear isomorphism onto the model fiber given by the trivialization $i$, and $|\cdot|$ the norm on $F$. Let ${f_i}_{i \in B}$ be a smooth partition of unity subordinate to the trivialization domains. Then the set ${v \in E_b : g_b(v,v) < 1}$ is bounded, where $g_b(v,v) = \sum_i f_i(b), |e_i v|^2$.

Since the $f_i(b)$ sum to $1$, at least one is positive; fix such an $i$, so $f_i(b) > 0$, and write $e := e_i$. Because $f_i(b) > 0$, the point $b$ lies in the support of $f_i$, and subordinacy places that support inside the small set where the trivialization $e$ is available.

For any $v$ in our set, the single $i$-th term is at most the whole sum: $f_i(b) |e v|^2 \le g_b(v,v) \lt 1$.

Since $f_i(b) > 0$, we can divide to obtain

$$|e v| \le \sqrt{\tfrac{1}{f_i(b)}}.$$

Setting $r = {1}/{f_i(b)}$, every $v$ in our set satisfies $e v \in \overline{B}_F!\big(0, r\big)$, and since $v = e^{-1}(e v)$ lies in $e^{-1}$ of that closed ball. Our set is therefore contained in the image of a bounded ball under the continuous linear map $e^{-1}$. That image is bounded (continuous linear maps preserve boundedness), and a subset of a bounded set is bounded.

---

[github-actions]

PR summary c4cbb8b896

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.ExistsRiemannianMetric (new file)	2583

---

Declarations diff (regex)

+ evalAt
+ exists_riemannian_metric
+ g_bilin
+ g_bilin_aux
+ g_bilin_aux_apply
+ g_bilin_aux_of_not_mem
+ g_bilin_smooth_on_chart
+ g_bilin_symm_aux
+ g_global_bilin
+ g_global_bilin_aux
+ g_global_bilin_aux_apply_eq
+ g_global_bilin_aux_support_finite
+ g_global_bilin_aux_term_le
+ g_global_bilin_aux_term_support_finite
+ g_global_bilin_eq
+ g_global_bilin_smooth
+ g_nonneg
+ g_pos
+ inCoordinates_apply_eq₂_spec
+ inCoordinates_apply_eq₂_spec_symm
+ map_finprod_of_mulSupport_subset
+ riemannian_metric_pos_def
+ riemannian_metric_pos_def_aux
+ riemannian_metric_symm
+ riemannian_metric_symm_aux
+ riemannian_unit_ball_bounded
+ riemannian_unit_ball_bounded_aux
+ smul_term_eq

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit c4cbb8b).

• +3 new declarations
• −0 removed declarations

+exists_riemannian_metric
+map_finprod_of_mulSupport_subset
+map_finsum_of_support_subset

---

Increase in strong tech debt: (relative, absolute) = (4.00, 1.00)

Current number	Change	Type (strong)
4	4	maxHeartBeats modifications

No changes to weak technical debt.

Current commit c4cbb8b896
Reference commit 65fe2a1f85

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[idontgetoutmuch]

From #33519 (comment)

(2) It would be good to generalise this argument to arbitrary vector bundles. Mathematically, there should be no meaningful difference. Would you like help with that/what happens when you try to do so?

Yes please but I do use the fact that the trivialisation of the bundle of bilinear forms is essentially given by the trivialisation of the tangent bundle. Maybe this can be generalised but off the top of my head, I don't know how.

I would think the analogous fact is true in any vector bundle (and this would be a useful lemma to have, independently of this PR --- i.e., a good pre-requisite PR).

@grunweg do you mean generalising this?

/-
Overloading the use of π, let φ : π⁻¹(U) → U × ℝⁿ and ψ : π⁻¹(U) → U × (ℝⁿ ⊗ ℝⁿ →ₗ ℝ) be local
trivialisations of the tangent bundle and the bundle of bilinear forms respectively and
w ∈ π⁻¹(U) and (x, u) and (y, v) ∈ U × ℝⁿ then ψ(w)(u, v) = w(φ⁻¹(x, u), φ⁻¹(x, v))
-/
lemma trivializationAt_tangentSpace_bilinearForm_apply (x₀ x : B)
    (w : (TangentSpace (M := B) IB) x →L[ℝ] (TangentSpace (M := B) IB) x →L[ℝ] ℝ)
    (u v : EB)
    (hx : x ∈ (trivializationAt EB (TangentSpace (M := B) IB) x₀).baseSet) :
  (trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
                    (fun x ↦ (TangentSpace (M := B) IB) x →L[ℝ]
                             (TangentSpace (M := B) IB) x →L[ℝ]
                              ℝ) x₀).continuousLinearMapAt ℝ x w u v =
  w ((trivializationAt EB (TangentSpace (M := B) IB) x₀).symm x u)
    ((trivializationAt EB (TangentSpace (M := B) IB) x₀).symm x v)

Code here:

mathlib4/Mathlib/Geometry/Manifold/ExistsRiemannianMetricTangentSpace.lean

Line 188 in 267f48f

lemma trivializationAt_tangentSpace_bilinearForm_apply (x₀ x : B)

[grunweg]

You know what your comment refers to - but this seems about right.

[idontgetoutmuch]

See also #28056

[grunweg]

Thanks for your PR; this result is sorely missing from mathlib.
I have two kinds of comments. The first one is that the code is not yet at mathlib's quality bar; it can be shortened significantly, for instance. I have made some example comments below. The second, higher-level, comment is that this result holds on any finite rank vector bundle --- hence should be proven in that generality. Would you like to attempt this generalisation also? As-is, this PR probably should not get merged.

[idontgetoutmuch]

I have been thinking about the comment on generalisation. But can this be generalised? What would the statement of a general theorem be? Existence of an n-form on a manifold?

/--
Existence of a smooth Riemannian metric on a manifold.
-/
public noncomputable
def riemannian_metric_exists
    (f : SmoothPartitionOfUnity B IB B)
    (h_sub : f.IsSubordinate (fun x ↦ (extChartAt IB x).source)) :
    ContMDiffRiemannianMetric (IB := IB) (n := ∞) (F := EB)
     (E := TangentSpace (M := B) IB) :=
  { inner := g_global_bilin_1 f
    symm := by
      exact riemannian_metric_symm_1 f
    pos := riemannian_metric_pos_def_1 f h_sub
    isVonNBounded := riemannian_unit_ball_bounded_1 f h_sub
    contMDiff := (g_global_bilin_1_smooth f h_sub)
     }

Moreover the proof relies on inCoordinates_apply_eq₂.

[grunweg]

You want to prove the existence of a Riemannian metric, on any vector bundle. (Let's say finite-dimensional for now.)

import Mathlib.Geometry.Manifold.VectorBundle.Riemannian

open Bundle ContDiff Manifold

-- Let E be a smooth vector bundle over a manifold E
variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
  {E : B → Type*} [TopologicalSpace (TotalSpace F E)]
  [∀ x, TopologicalSpace (E x)] [∀ x, AddCommGroup (E x)] [∀ x, Module ℝ (E x)]
  [FiberBundle F E] [VectorBundle ℝ F E]
  [IsManifold IB n B] [ContMDiffVectorBundle n F E IB]

noncomputable def foo
    [∀ x, FiniteDimensional ℝ (E x)] [∀ x, ContinuousAdd (E x)] [∀ x, ContinuousSMul ℝ (E x)] :
    ContMDiffRiemannianMetric IB ∞ F E where
  inner := sorry
  symm b := sorry
  pos b := sorry
  isVonNBounded b := sorry
  contMDiff := sorry

I don't see the issues with inCoordinates_apply_eq; it is already stated and proven for general Hom bundles.

[idontgetoutmuch]

You want to prove the existence of a Riemannian metric, on any vector bundle. (Let's say finite-dimensional for now.)

import Mathlib.Geometry.Manifold.VectorBundle.Riemannian

open Bundle ContDiff Manifold

-- Let E be a smooth vector bundle over a manifold E
variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
  {E : B → Type*} [TopologicalSpace (TotalSpace F E)]
  [∀ x, TopologicalSpace (E x)] [∀ x, AddCommGroup (E x)] [∀ x, Module ℝ (E x)]
  [FiberBundle F E] [VectorBundle ℝ F E]
  [IsManifold IB n B] [ContMDiffVectorBundle n F E IB]

noncomputable def foo
    [∀ x, FiniteDimensional ℝ (E x)] [∀ x, ContinuousAdd (E x)] [∀ x, ContinuousSMul ℝ (E x)] :
    ContMDiffRiemannianMetric IB ∞ F E where
  inner := sorry
  symm b := sorry
  pos b := sorry
  isVonNBounded b := sorry
  contMDiff := sorry

I don't see the issues with inCoordinates_apply_eq; it is already stated and proven for general Hom bundles.

Thank you. I have been barking up the wrong generalisation tree (auf dem Holzweg). That feels like it should be easy enough. Yes inCoordinates_apply_eq should cause no problems,

[idontgetoutmuch]

@grunweg thanks for all the feedback - I am working through generalising everything and then I will address your feedback (which may no longer apply if we are lucky).

[idontgetoutmuch]

Thanks for your PR; this result is sorely missing from mathlib. I have two kinds of comments. The first one is that the code is not yet at mathlib's quality bar; it can be shortened significantly, for instance. I have made some example comments below. The second, higher-level, comment is that this result holds on any finite rank vector bundle --- hence should be proven in that generality. Would you like to attempt this generalisation also? As-is, this PR probably should not get merged.

All generalised now but my refactoring technique now needs cosmetic attention. I will address all comments and then perhaps you can help with getting the code to the quality bar (is this just someone's opinion? in which case whose?).

[idontgetoutmuch]

I think I addressed all the comments so I've removed the "awaiting author" label.

[idontgetoutmuch]

Maybe I should add

theorem exists_riemannian_metric
  [FiniteDimensional ℝ F]
  [∀ x, FiniteDimensional ℝ (E x)] :
    Nonempty (ContMDiffRiemannianMetric (IB := IB) (n := ∞) (F := F) (E := E)) :=
  let ⟨f, hf⟩ := exists_partition_subordinate_to_intersection (F := F)
  ⟨riemannian_metric_exists f hf⟩

Every smooth finite-dimensional vector bundle over a smooth manifold admits a smooth Riemannian metric on its fibers.

[grunweg]

All generalised now but my refactoring technique now needs cosmetic attention. I will address all comments and then perhaps you can help with getting the code to the quality bar (is this just someone's opinion? in which case whose?).

Congratulations on completing the generalisation! I'll be happy to help you raise the code towards mathlib quality. (Perhaps I can take a look again later today.)

A lot of the quality bar is documented in the style guide, the rest is accumulated collective wisdom on writing code that is maintainable in the long term. There is broad consensus on that. In principle, any maintainer has the power to unilaterally merge a PR. In practice, we operate by consensus (and discuss potentially controversial topics beforehand).

[grunweg]

I have looked at your PR from a style/golfing perspective: I think it can be written more compactly, which makes it easier to see what's going on, and to maintain the proof going forward. I have a number of such suggestions. Often, each case occurs many times throughout your PR, and I have said so: please try to look for other occurrences and fix those as well. Thank you!

Let me emphasize that most of these comments should be quick to address, and will make it easier to review the code in more detail.

[grunweg]

Thanks for your changes - it's generally moving in the right direction. (I think the many different variable lines can be cleaned up a bit, but if needed I can take a pass at that.)

I have a few more comments. Some of them are pointing at previous comments of mine - can you check that you took a look at them all?

[grunweg]

Some more comments. Trying them locally, something breaks --- so be careful to test that each of your changes is fine. (Perhaps make changes outside instances first; those should be safe.)

The fact that "something breaks" is a warning sign; there'll be the need to debug why. I won't have time for that this week, and fixing some style issues first is a good idea in any case.

[grunweg]

Please indent these lines like so (likewise below)

Suggested change

	(φ : E x →L[ℝ] E x →L[ℝ] ℝ)
	(hpos : ∀ v, 0 ≤ φ v v)
	(hsymm : ∀ u v, φ u v = φ v u)
	(hdef : ∀ v, φ v v = 0 → v = 0)
	(u v : VectorSpaceAux x φ hpos hsymm hdef) :
	u = v ↔ u.val = (v.val : E x) := by
	(φ : E x →L[ℝ] E x →L[ℝ] ℝ)
	(hpos : ∀ v, 0 ≤ φ v v)
	(hsymm : ∀ u v, φ u v = φ v u)
	(hdef : ∀ v, φ v v = 0 → v = 0)
	(u v : VectorSpaceAux x φ hpos hsymm hdef) :
	u = v ↔ u.val = (v.val : E x) := by

All of these are hypotheses for the lemma, or the lemma statement. If the whole statement spans multiple lines, they should be indented by four spaces (or four plus x, if there is further indentation of x required).

[idontgetoutmuch]

Like this a0e3c66? Then I should do the same for the other lemmas in this section?

[grunweg]

Please also indent the u = v ↔ u.val = (v.val : E x) := by line.

With that fixes: yes, please do the same for the other lemmas in the section.

[grunweg]

Thanks; this is going into the right direction. Feel free to write a comment once you have addressed all comments; then I can take a look again.

[tb65536]

Indentation is wrong here.

[tb65536]

Suffices would be better than a long have here.

[tb65536]

Indentation is wrong here.

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[grunweg]

Thanks, this PR is definitely making progress. The next step (in my opinion) is to split out pieces that can be reviewed independently. For instance, inCoordinates_apply_eq₂_spec and inCoordinates_apply_eq₂_spec_symm should move to a more basic file, and could be a preliminary PR.

(I'll also note that you have a handful of yet unaddressed small review comments.)

[grunweg]

Inline this, please --- the proof gets slightly shorter without :-)

[grunweg]

Can you move this lemma and the next to a more basic file? They apply more broadly than Riemannian metrics.