feat(Mathlib/Geometry/Manifold): Riemannian metrics exist II

[idontgetoutmuch]

Supersedes #33519

---

[github-actions]

PR summary 0e708caf75

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.ExistsRiemannianMetricTangentSpace (new file)	2403

---

Declarations diff

+ TangentSpaceAux
+ TangentSpaceAux.ext_iff
+ aux
+ aux_tvs
+ contMDiff_totalSpace_weighted_sum_of_local_sections
+ evalAt
+ exists_partition_subordinate_to_intersection
+ finsum_image_eq_sum
+ g_bilin_1g
+ g_bilin_1g_smooth_on_chart
+ g_bilin_2g
+ g_bilin_eq''
+ g_bilin_eq_00a_pre
+ g_bilin_symm_2
+ g_global_bilin_1'
+ g_global_bilin_1_smooth'
+ g_global_bilin_2'
+ g_global_bilin_eq'
+ g_nonneg'
+ g_pos'
+ h_need
+ h_need'''
+ instance {x : B} (φ : E x →L[ℝ] E x →L[ℝ] ℝ)
+ linear_flip_apply
+ my_dist_triangle
+ my_eq_of_dist_eq_zero
+ riemannian_metric_def''
+ riemannian_metric_exists'
+ riemannian_metric_pos_def'
+ riemannian_metric_pos_def_1'
+ riemannian_metric_symm
+ riemannian_metric_symm_1'
+ riemannian_unit_ball_bounded''
+ riemannian_unit_ball_bounded_1'
+ seminormOfBilinearForm
+ seminormOfBilinearForm_sub_comm
+ seminormOfBilinearForm_sub_self
+ tangentSpaceEquiv
+ trivializationAt_vectorBundle_bilinearForm_apply
+ withSeminormsOfBilinearForm
+++++++++ instance {x : B}

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/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.

[grunweg]

Same here

[grunweg]

I'd write noncomputable section here, and drop all the noncomputable keywords below

[grunweg]

It's better to avoid tactics to construct definitions --- in particular, if is slightly better than by_cases here. I'd write this as a proof term:

Suggested change

	noncomputable
	def g_bilin_1 (i b : B) :
	(TotalSpace (EB →L[ℝ] EB →L[ℝ] ℝ)
	(fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)) := by
	let ψ := FiberBundle.trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
	(fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ) i
	by_cases h : (b, (fun (x : B) ↦ innerSL ℝ) b) ∈ ψ.target
	· exact ψ.invFun (b, (fun (x : B) ↦ innerSL ℝ) b)
	· exact ⟨b, 0⟩
	def g_bilin_1 (i b : B) :
	(TotalSpace (EB →L[ℝ] EB →L[ℝ] ℝ)
	(fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)) := by
	letI ψ := FiberBundle.trivializationAt (EB →L[ℝ] EB →L[ℝ] ℝ)
	(fun (x : B) ↦ TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ) i
	by_cases h : (b, (fun (x : B) ↦ innerSL ℝ) b) ∈ ψ.target
	· exact ψ.invFun (b, (fun (x : B) ↦ innerSL ℝ) b)
	· exact ⟨b, 0⟩

Note the use of letI, which gives you better proof terms.

[grunweg]

inner is unused, so can be removed. With the same procedure as above, I arrive at

  letI χ := trivializationAt EB (TangentSpace (M := B) IB) i
  if h : p ∈ χ.baseSet then
    (innerSL ℝ).comp (χ.continuousLinearMapAt ℝ p) |>.flip.comp (χ.continuousLinearMapAt ℝ p)
  else 0

[grunweg]

In this lemma, simp is working against you because you're working with the tangent bundle: this simp simplifies the baseSet to something involving (chartAt HB x₀).source, and then you need to convert it back using hx'. This will go away when you work with general bundles.

[grunweg]

h1 is only used once and can be inlined below

[grunweg]

The mathlib style guide has a rule "hypothesis left of colon": applied here, it would yield

Suggested change

	have h4 : ∀ u v,
	have h4 (u v) :
	(((Trivialization.continuousLinearMapAt ℝ ψ b) (ψ.symmL ℝ b (innerSL ℝ))) u) v =
	innerSL ℝ u v := by
	rw [Trivialization.continuousLinearMapAt_symmL ψ hc]

[grunweg]

No need for specifying M again.

[grunweg]

In general, this proof is very long --- and my intuition is that it should be shortened. If the haves cannot be inlined easily, that's to be investigated.

[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).