Skip to content

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

Open
grunweg wants to merge 27 commits intoleanprover-community:masterfrom
grunweg:gramSchmidt-sections-smooth
Open

feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections#27025
grunweg wants to merge 27 commits intoleanprover-community:masterfrom
grunweg:gramSchmidt-sections-smooth

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jul 12, 2025 •
edited
Loading

For the Gram-Schmidt process on a vector bundle, deduce that smoothness of the bundle metric implies smoothness of the resulting sections.

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

A few sorries remain to prove the continuous case.

Open in Gitpod

@grunweg
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).
@grunweg grunweg mentioned this pull request Jul 12, 2025
Draft
35 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 12, 2025 •
edited
Loading

PR summary 0ccc06d21e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Manifold.Traces (new file) 1
Mathlib.Geometry.Manifold.Elaborators (new file) 1980
Mathlib.Geometry.Manifold.VectorBundle.GramSchmidtOrtho (new file) 2107

Declarations diff

+ ContMDiffWithinAt.starProjection
+ ContinuousWithinAt.starProjection
+ _root_.Lean.Expr.getUniverse
+ coe_gramSchmidtBasis
+ coe_gramSchmidtNormedBasis
+ contMDiffAt_aux
+ contMDiffWithinAt_aux
+ contMDiffWithinAt_inner
+ continuousAt_aux
+ continuousWithinAt_aux
+ continuousWithinAt_inner
+ find_model
+ gramSchmidt
+ gramSchmidtBasis
+ gramSchmidtNormed
+ gramSchmidtNormedBasis
+ gramSchmidtNormed_apply_of_orthogonal
+ gramSchmidtNormed_apply_of_orthonormal
+ gramSchmidtNormed_coe
+ gramSchmidtNormed_contMDiff
+ gramSchmidtNormed_contMDiffAt
+ gramSchmidtNormed_contMDiffOn
+ gramSchmidtNormed_contMDiffWithinAt
+ gramSchmidtNormed_continuous
+ gramSchmidtNormed_continuousAt
+ gramSchmidtNormed_continuousOn
+ gramSchmidtNormed_continuousWithinAt
+ gramSchmidtNormed_linearIndependent
+ gramSchmidtNormed_orthonormal
+ gramSchmidtNormed_orthonormal'
+ gramSchmidtNormed_unit_length'
+ gramSchmidtOrthonormalBasis
+ gramSchmidtOrthonormalBasis_apply_of_orthonormal
+ gramSchmidtOrthonormalBasis_coe
+ gramSchmidt_apply
+ gramSchmidt_bot
+ gramSchmidt_contMDiff
+ gramSchmidt_contMDiffAt
+ gramSchmidt_contMDiffOn
+ gramSchmidt_contMDiffWithinAt
+ gramSchmidt_continuous
+ gramSchmidt_continuousAt
+ gramSchmidt_continuousOn
+ gramSchmidt_continuousWithinAt
+ 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
+ mkApp12
+ 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).

@grunweg grunweg added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-differential-geometry Manifolds etc labels Jul 12, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jul 12, 2025 •
edited
Loading

This PR/issue depends on:

@grunweg grunweg force-pushed the gramSchmidt-sections-smooth branch 4 times, most recently from d279fc5 to c1e6efc Compare July 15, 2025 14:09
@grunweg grunweg mentioned this pull request Jul 15, 2025
Open
1 task
grunweg and others added 2 commits July 15, 2025 16:38
@grunweg @faenuccio
Apply suggestions from code review
13759b5 
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
@grunweg
Comment on the implementation choice
f18f331
faenuccio
faenuccio reviewed Jul 15, 2025
View reviewed changes
@leanprover-community-bot-assistant 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
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

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

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

@grunweg grunweg force-pushed the gramSchmidt-sections-smooth branch from 912e7a0 to 78bc816 Compare July 29, 2025 14:17
@github-actions github-actions bot 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 29, 2025
@grunweg grunweg force-pushed the gramSchmidt-sections-smooth branch from 78bc816 to 6dfe730 Compare July 29, 2025 14:18
@grunweg grunweg mentioned this pull request Jul 30, 2025
Open
2 tasks
@mathlib4-merge-conflict-bot 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 Nov 16, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 16, 2025

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@faenuccio faenuccio faenuccio left review comments

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@grunweg @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @mathlib4-merge-conflict-bot @faenuccio