feat: the index of Fredholm operators is locally constant

[ADedecker]

---

• depends on: feat: the set of Fredholm operators between two Banach spaces is open #42742

[github-actions]

PR summary b3a6706f15

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Operator.Fredholm.Basic	2052	2054	+2 (+0.10%)

Import changes for all files

Files	Import difference
243 files Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Module.ZLattice.Summable Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.DerivNotation Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.CanonicalTensor Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Continuous Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.MulOpposite Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection.Basic Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional Mathlib.Analysis.InnerProductSpace.Projection.Reflection Mathlib.Analysis.InnerProductSpace.Projection.Submodule Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.Matrix.Hermitian Mathlib.Analysis.Matrix.Normed Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Field.Dense Mathlib.Analysis.Normed.Field.Krasner Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative Mathlib.Analysis.Normed.Unbundled.SpectralNorm Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.Real.Pi.Chudnovsky Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.Randomisation Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircleAdd Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Extreme Mathlib.Dynamics.Ergodic.RadonNikodym Mathlib.Geometry.Euclidean.Altitude Mathlib.Geometry.Euclidean.Angle.Bisector Mathlib.Geometry.Euclidean.Angle.Incenter Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.Projection Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Incenter Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.NinePointCircle Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Projection Mathlib.Geometry.Euclidean.SignedDist Mathlib.Geometry.Euclidean.Similarity Mathlib.Geometry.Euclidean.Simplex Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.OrthRadius Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Sphere.Tangent Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Euclidean.Volume.Measure Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Stochastic Mathlib.LinearAlgebra.Matrix.Swap Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.BorelGrowth Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.Holder Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.IntegralConvolution Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Group.ModularCharacter Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner.Basic Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus Mathlib.MeasureTheory.Integral.Bochner.L1 Mathlib.MeasureTheory.Integral.Bochner.Set Mathlib.MeasureTheory.Integral.Bochner.SumMeasure Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CompactlySupported Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.FinMeasAdditive Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.MeanValue Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.Regular Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real Mathlib.MeasureTheory.Integral.SetToL1.ChangeMeasure Mathlib.MeasureTheory.Integral.SetToL1.DominatedConvergence Mathlib.MeasureTheory.Integral.SetToL1.Function Mathlib.MeasureTheory.Integral.SetToL1.L1 Mathlib.MeasureTheory.Integral.SetToL1.SimpleFunc Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Measure.CharacteristicFunction Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasurePi Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.DistribChar Mathlib.MeasureTheory.Measure.Haar.Extension Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Prokhorov Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.TightNormed Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap Mathlib.MeasureTheory.SpecificCodomains.Pi Mathlib.MeasureTheory.SpecificCodomains.WithLp Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym Mathlib.MeasureTheory.VectorMeasure.Integral Mathlib.MeasureTheory.VectorMeasure.Prod Mathlib.MeasureTheory.VectorMeasure.SetIntegral Mathlib.MeasureTheory.VectorMeasure.WithDensityVec Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.Padics.Complex Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.WellApproximable Mathlib.Probability.CDF Mathlib.Probability.Density Mathlib.Probability.Distributions.Fernique Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Independence.Integrable Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.SetIntegral Mathlib.Probability.Kernel.WithDensity Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.ContinuousAlternatingMap Mathlib.Topology.VectorBundle.FiniteDimensional Mathlib.Topology.VectorBundle.Hom Mathlib.Topology.VectorBundle.Riemannian	1
Mathlib.Analysis.Normed.Operator.Fredholm.Basic	2
Mathlib.Analysis.Normed.Operator.Fredholm.Open (new file)	2121

---

Declarations diff (regex)

+ ContinuousLinearEquiv.isOpen
+ ContinuousLinearEquiv.nhds
+ ContinuousLinearMap.IsInvertible.eventually
+ ContinuousLinearMap.isOpen_setOfPred_isInvertible
+ FredholmPackage.eventually_isInvertible
+ IsFredholm.eventually
+ IsFredholm.eventually_and_index_eq
+ IsFredholm.eventually_index_eq
+ IsFredholm.index_comp
+ IsIdempotentElem.isFredholm
+ IsIdempotentElem.isFredholm_iff
+ _root_.FredholmDecomposition.cofg_X₁
+ _root_.FredholmDecomposition.isFredholm_proj
+ _root_.Submodule.isFredholm_projectionL
+ _root_.Submodule.isFredholm_projectionL_iff
+ _root_.Submodule.isFredholm_projectionOntoL
+ _root_.Submodule.isFredholm_projectionOntoL_iff
+ index_of_bijective
+ isOpen_setOfPred_isFredholm
+ isQuotientMap_projectionOnto
- isOpen
- nhds

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 -- pending)

Computed after the build finishes.

---

Decrease in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
backward.isDefEq.respectTransparency.types	2526	-1

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	4968	1

Current commit b3a6706f15
Reference commit 8b36e86753

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: the set of Fredholm operators between two Banach spaces is open #42742
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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