feat: Gram-Schmidt orthonormalisation for sections of a vector bundle by grunweg · Pull Request #27024 · leanprover-community/mathlib4

grunweg · 2025-07-12T09:06:21Z

Add a parametrised version of Gram-Schmidt, for sections of a topological vector bundle with a bundle metric.
This will be used to define orthonormal local frames.

From the path towards geodesics and the Levi-Civita connection.
Co-authored-by: Patrick Massot patrickmassot@free.fr

depends on: [Merged by Bors] - feat: gramSchmidtNormed_linearIndependent and minor tweaks #27023

Add gramSchmidt_zero (about gramSchmidt applied to a set of zero vectors), rename the previous gramSchmidt_zero to gramSchmidt_bot (which is the correct name anyway).

github-actions · 2025-07-12T09:07:30Z

PR summary 0ccc06d21e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Topology.VectorBundle.GramSchmidtOrtho` (new file)	2018

Declarations diff

+ coe_gramSchmidtBasis
+ coe_gramSchmidtNormedBasis
+ gramSchmidt
+ gramSchmidtBasis
+ gramSchmidtNormed
+ gramSchmidtNormedBasis
+ gramSchmidtNormed_apply_of_orthogonal
+ gramSchmidtNormed_apply_of_orthonormal
+ gramSchmidtNormed_coe
+ gramSchmidtNormed_linearIndependent
+ gramSchmidtNormed_orthonormal
+ gramSchmidtNormed_orthonormal'
+ gramSchmidtNormed_unit_length'
+ gramSchmidtOrthonormalBasis
+ gramSchmidtOrthonormalBasis_apply_of_orthonormal
+ gramSchmidtOrthonormalBasis_coe
+ gramSchmidt_apply
+ gramSchmidt_bot
+ gramSchmidt_def
+ gramSchmidt_def'
+ gramSchmidt_def''
+ gramSchmidt_inv_triangular
+ gramSchmidt_linearIndependent
+ gramSchmidt_mem_span
+ gramSchmidt_ne_zero
+ gramSchmidt_ne_zero_coe
+ gramSchmidt_orthogonal
+ gramSchmidt_pairwise_orthogonal
+ gramSchmidt_zero
+ mem_span_gramSchmidt
+ span_gramSchmidt
+ span_gramSchmidtNormed
+ span_gramSchmidtNormed_range
+ span_gramSchmidt_Iic
+ span_gramSchmidt_Iio
+-+ gramSchmidt_of_orthogonal
-++ gramSchmidtNormed_unit_length
-++ gramSchmidtNormed_unit_length_coe

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 script/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).

faenuccio

Thanks!

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean

faenuccio

I have not noticed that a part of this was in #27023, so I made my comments to that PR for this one.

Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

grunweg

Thank you for the detailed review! I just followed most of your suggestions; here are a few comments about some of your questions.

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean

faenuccio · 2025-07-15T13:53:42Z

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean

+
+open Finset
+
+namespace VectorBundle


I agree, and I've seen your changes. But although I agree that having B simply a top. manifold seems ok, having E a top. vector bundle might cause problems when you will need to prove that GS preserves regularity, no?

Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

grunweg · 2025-07-15T14:51:46Z

This is ready for review again.

leanprover-community-bot-assistant · 2025-07-16T12:17:25Z

This pull request has conflicts, please merge master and resolve them.

grunweg · 2025-07-17T13:36:32Z

CI passes now

faenuccio

You're right, this projection is missing (and should be added).
I don't think that would really help, though --- for topological vector bundles, you rather want a result that applying Gram-Schmidt to continuous sections yields something continuous, don't you? (I've started on this in #27025, but this uncovered some amount of missing basic API. So adding this may require a bit more tedium than I'd like for now.)

I think I did not make myself clear. What I am saying is that if now your assumption is [IsContinuousRiemannianBundle] and you lack IsContMDiffRiemannianBundle.toIsContinuousRiemannianBundle, how can you apply the results in this file to a ContMDiffRiemanianBundle?

grunweg · 2025-07-30T10:41:07Z

You're right, this projection is missing (and should be added).
I don't think that would really help, though --- for topological vector bundles, you rather want a result that applying Gram-Schmidt to continuous sections yields something continuous, don't you? (I've started on this in #27025, but this uncovered some amount of missing basic API. So adding this may require a bit more tedium than I'd like for now.)

I think I did not make myself clear. What I am saying is that if now your assumption is [IsContinuousRiemannianBundle] and you lack IsContMDiffRiemannianBundle.toIsContinuousRiemannianBundle, how can you apply the results in this file to a ContMDiffRiemanianBundle?

Yes, that clarification helped. Are you fine with a "constructive proof"? #27025 applies these results to a C^n Riemannian bundle, and works. (#print axioms gramSchmidtNormed_contMDiff returns "'gramSchmidtNormed_contMDiff' depends on axioms: [propext, Classical.choice, Quot.sound]", i.e. is sorry-free.)

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean

Mathlib/Topology/VectorBundle/GramSchmidtOrtho.lean

sgouezel

Could you explain a little bit why duplicating the API of InnerProductSpace.gramSchmidt to VectorBundle.gramSchmidt is useful? (That's an honest question: most of the file seems to be just a restatement of preexisting lemmas, but I'm sure you have encountered difficulties when trying to work just with InnerProductSpace.gramSchmidt, which prompted you to this duplication)

sgouezel · 2025-08-07T10:32:59Z

Mathlib/Topology/VectorBundle/GramSchmidtOrtho.lean

+/-- The Gram-Schmidt process takes a set of sections as input
+and outputs a set of sections which are point-wise orthogonal and have the same span.
+Basically, we apply the Gram-Schmidt algorithm point-wise. -/
+noncomputable def gramSchmidt (s : ι → (x : B) → E x) (n : ι) : (x : B) → E x :=


move x left of the colon?

sgouezel · 2025-08-10T13:12:50Z

Mathlib/Topology/VectorBundle/GramSchmidtOrtho.lean

+
+/-- If the section values `s i x` are orthogonal, `gramSchmidt` yields the same values at `x`. -/
+theorem gramSchmidt_of_orthogonal (hs : Pairwise fun i j ↦ ⟪s i x, s j x⟫ = 0) :
+    ∀ i₀, gramSchmidt s i₀ x = s i₀ x := by


move i0 left of the colon?

faenuccio · 2025-08-13T11:57:11Z

You're right, this projection is missing (and should be added).
I don't think that would really help, though --- for topological vector bundles, you rather want a result that applying Gram-Schmidt to continuous sections yields something continuous, don't you? (I've started on this in #27025, but this uncovered some amount of missing basic API. So adding this may require a bit more tedium than I'd like for now.)

I think I did not make myself clear. What I am saying is that if now your assumption is [IsContinuousRiemannianBundle] and you lack IsContMDiffRiemannianBundle.toIsContinuousRiemannianBundle, how can you apply the results in this file to a ContMDiffRiemanianBundle?

Yes, that clarification helped. Are you fine with a "constructive proof"? #27025 applies these results to a C^n Riemannian bundle, and works. (#print axioms gramSchmidtNormed_contMDiff returns "'gramSchmidtNormed_contMDiff' depends on axioms: [propext, Classical.choice, Quot.sound]", i.e. is sorry-free.)

I am certainly happy with such a constructive proof! But I confess I do not understand how it can possibly work. EDIT I had a closer look, and it seems to me that in that file at the beginning of the section smoothness you re-introduce all your gadgets (in particular, you declare a variable F : Type* and variable [IsContMDiffRiemannianBundle IB n F E] but the old ones are still in force, so you have both [IsContMDiffRiemannianBundle IB n F E] and [IsContinuousRiemannianBundle F E] in force.

mathlib4-merge-conflict-bot · 2025-09-15T13:21:54Z

This pull request has conflicts, please merge master and resolve them.

feat: gramSchmidtNormed_linearIndependent and minor tweaks

2923cdc

Add gramSchmidt_zero (about gramSchmidt applied to a set of zero vectors), rename the previous gramSchmidt_zero to gramSchmidt_bot (which is the correct name anyway).

This was referenced Jul 12, 2025

Mr. Covariant Derivatives #26221

Draft

feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections #27025

Open

feat: Gram-Schmidt process on sections of a vector bundle

c7cba64

grunweg force-pushed the gramSchmidt-sections branch from 7a2d3c8 to c7cba64 Compare July 12, 2025 09:14

grunweg added the t-differential-geometry Manifolds etc label Jul 12, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 12, 2025

grunweg added 2 commits July 12, 2025 11:37

Lint, micro-shake

dadf8c3

Noshake

38e8631

faenuccio reviewed Jul 15, 2025

View reviewed changes

faenuccio added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 15, 2025

grunweg and others added 4 commits July 15, 2025 13:25

Apply suggestions from code review

490b28e

Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

Apply suggestions from code review

c4bad06

Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

More review comments

d1a968e

Further tweaks to InnerProductSpace/GramSchmidtOrtho

9f55821

grunweg commented Jul 15, 2025

View reviewed changes

grunweg added 3 commits July 15, 2025 13:51

More small tweaks

af6e8f2

Wording

41d8b8b

Final clean-up, mostly around variable implicitness

ac75e88

grunweg commented Jul 15, 2025

View reviewed changes

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean Outdated Show resolved Hide resolved

grunweg added 3 commits July 15, 2025 15:28

Make n implicit

a83d63e

Inline explicit s: it's short, and more readable/standard this way

eb35ab4

Generalise to topological vector bundles

144fd29

faenuccio reviewed Jul 15, 2025

View reviewed changes

Apply suggestions from code review

13759b5

Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 15, 2025

Comment on the implementation choice

f18f331

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 16, 2025

Merge branch 'master' into gramSchmidt-sections

16d07a7

grunweg removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 16, 2025

Fixes and tweaks

7d20634

faenuccio reviewed Jul 17, 2025

View reviewed changes

grunweg added 3 commits July 29, 2025 16:09

Merge branch 'master' into gramSchmidt-sections

381b47c

Fix merge

e1e1480

Tweak

5002de9

sgouezel reviewed Jul 30, 2025

View reviewed changes

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean Show resolved Hide resolved

sgouezel reviewed Jul 30, 2025

View reviewed changes

Mathlib/Geometry/Manifold/VectorBundle/GramSchmidtOrtho.lean Outdated Show resolved Hide resolved

Remove unused variables

ebb2993

grunweg mentioned this pull request Jul 30, 2025

feat: Gram-Schmidt orthonormalisation preserves continuity of sections #27694

Open

2 tasks

Move

f37285e

grunweg commented Jul 31, 2025

View reviewed changes

Mathlib/Topology/VectorBundle/GramSchmidtOrtho.lean Outdated Show resolved Hide resolved

grunweg added 5 commits July 31, 2025 10:16

Update Mathlib/Topology/VectorBundle/GramSchmidtOrtho.lean

c0b8f43

Noshake

0f29f29

Shake

87af5cd

Minimise more

bc11636

Noshake

b0fb43b

grunweg assigned hrmacbeth and sgouezel and unassigned hrmacbeth Jul 31, 2025

sgouezel reviewed Aug 10, 2025

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 14, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 15, 2025


		open Finset

		namespace VectorBundle

Conversation

grunweg commented Jul 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0ccc06d21e

Import changes for modified files

Declarations diff

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio Jul 15, 2025

Choose a reason for hiding this comment

Uh oh!

grunweg commented Jul 15, 2025

Uh oh!

leanprover-community-bot-assistant commented Jul 16, 2025

Uh oh!

grunweg commented Jul 17, 2025

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

grunweg commented Jul 30, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

sgouezel Aug 7, 2025

Choose a reason for hiding this comment

Uh oh!

sgouezel Aug 10, 2025

Choose a reason for hiding this comment

Uh oh!

faenuccio commented Aug 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Sep 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

grunweg commented Jul 12, 2025 •

edited

Loading

github-actions bot commented Jul 12, 2025 •

edited

Loading

faenuccio commented Aug 13, 2025 •

edited

Loading