feat: Gram-Schmidt orthonormalisation preserves continuity of sections

[grunweg]

provided the bundle metric used in the process is continuous.

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

---

• depends on: feat: Gram-Schmidt orthonormalisation for sections of a vector bundle #27024
• depends on: [Merged by Bors] - feat: custom elaborators for differential geometry #27021

Baby version of #27025.

[github-actions]

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.VectorBundle.GramSchmidtOrtho (new file)	2097

---

Declarations diff

+ ContinuousWithinAt.starProjection
+ coe_gramSchmidtBasis
+ coe_gramSchmidtNormedBasis
+ continuousAt_aux
+ continuousWithinAt_aux
+ continuousWithinAt_inner
+ gramSchmidt
+ gramSchmidtBasis
+ gramSchmidtNormed
+ gramSchmidtNormedBasis
+ gramSchmidtNormed_apply_of_orthogonal
+ gramSchmidtNormed_apply_of_orthonormal
+ gramSchmidtNormed_coe
+ 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_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
+ 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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: Gram-Schmidt orthonormalisation for sections of a vector bundle #27024
• [Merged by Bors] - feat: custom elaborators for differential geometry #27021
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

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