feat: constructions of Fredholm operators

[ADedecker]

Co-authored-by: @CoolRmal

---

• depends on: feat: composition of Fredholm operators #41601

[github-actions]

PR summary f4b8767841

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Maps.Strict.Module (new file)	1281
Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite (new file)	2020
Mathlib.Analysis.FredholmOperator (new file)	2123

---

Declarations diff (regex)

+ ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_eqOn
+ ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid
+ ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient
+ ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict
+ FredholmPackage
+ FredholmPackage.equiv_eq_restrict
+ FredholmPackage.isFredholm
+ FredholmPackage.isInvertible_restrict
+ FredholmPackage.isQuasiInverse
+ FredholmPackage.ker_eq
+ FredholmPackage.mapsTo
+ FredholmPackage.quasiInverse
+ FredholmPackage.range_eq
+ IsFredholm
+ IsFredholm.closedComplemented_range
+ IsFredholm.comp
+ IsFredholm.comp_iff_left
+ IsFredholm.comp_iff_right
+ IsFredholm.congr
+ IsFredholm.fredholmPackage
+ IsFredholm.id
+ IsFredholm.nonempty_fredholmPackage
+ IsFredholm.of_isInvertible_restrict
+ LinearMap.isClosed_range_of_isClosed_map_of_finiteDimensional_quotient
+ _root_.ContinuousLinearEquiv.isFredholm
+ _root_.ContinuousLinearEquiv.quotKerEquivRange
+ _root_.FredholmDecomposition
+ _root_.FredholmDecomposition.proj
+ _root_.Submodule.isFredholm_subtypeL
+ _root_.Submodule.mkQL_isFredholmStruct
+ _root_.Topology.IsClosedEmbedding.isFredholmStruct
+ _root_.Topology.IsQuotientMap.isFredholm
+ eqOn_eqLocus
+ exists_restrict_isInvertible_of_isQuasiInverse
+ isFredholm_congr
+ isFredholm_iff_exists_isQuasiInverse
+ isFredholm_tfae
+ isStrictMap_iff_isEmbedding_liftQ_ker
+ isStrictMap_iff_isHomeomorph_quotKerEquivRange
+ isStrictMap_iff_isOpenQuotientMap_rangeRestrict
+ isStrictMap_prodMap
+ isStrictMap_prodMap_iff
+ step1
+ step2
+ step3
+ step4

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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f4b8767).

• +84 new declarations
• −0 removed declarations

+ContinuousLinearEquiv.isFredholm
+ContinuousLinearEquiv.ofIsHomeomorph.congr_simp
+ContinuousLinearEquiv.quotKerEquivRange
+ContinuousLinearEquiv.quotKerEquivRange.congr_simp
+ContinuousLinearMap.FredholmPackage
+ContinuousLinearMap.FredholmPackage.casesOn
+ContinuousLinearMap.FredholmPackage.ctorIdx
+ContinuousLinearMap.FredholmPackage.decCodom
+ContinuousLinearMap.FredholmPackage.decDom
+ContinuousLinearMap.FredholmPackage.eq_equiv
+ContinuousLinearMap.FredholmPackage.equiv
+ContinuousLinearMap.FredholmPackage.equiv_eq_restrict
+ContinuousLinearMap.FredholmPackage.isFredholm
+ContinuousLinearMap.FredholmPackage.isInvertible_restrict
+ContinuousLinearMap.FredholmPackage.isQuasiInverse
+ContinuousLinearMap.FredholmPackage.ker_eq
+ContinuousLinearMap.FredholmPackage.mapsTo
+ContinuousLinearMap.FredholmPackage.mk
+ContinuousLinearMap.FredholmPackage.mk.inj
+ContinuousLinearMap.FredholmPackage.mk.injEq
+ContinuousLinearMap.FredholmPackage.mk.noConfusion
+ContinuousLinearMap.FredholmPackage.mk.sizeOf_spec
+ContinuousLinearMap.FredholmPackage.noConfusion
+ContinuousLinearMap.FredholmPackage.noConfusionType
+ContinuousLinearMap.FredholmPackage.quasiInverse
+ContinuousLinearMap.FredholmPackage.range_eq
+ContinuousLinearMap.FredholmPackage.rec
+ContinuousLinearMap.FredholmPackage.recOn
+ContinuousLinearMap.IsFredholm
+ContinuousLinearMap.IsFredholm.casesOn
+ContinuousLinearMap.IsFredholm.closedComplemented_ker
+ContinuousLinearMap.IsFredholm.closedComplemented_range
+ContinuousLinearMap.IsFredholm.comp
+ContinuousLinearMap.IsFredholm.comp_iff_left
+ContinuousLinearMap.IsFredholm.comp_iff_right
+ContinuousLinearMap.IsFredholm.congr
+ContinuousLinearMap.IsFredholm.finite_coker
+ContinuousLinearMap.IsFredholm.finite_ker
+ContinuousLinearMap.IsFredholm.fredholmPackage
+ContinuousLinearMap.IsFredholm.id
+ContinuousLinearMap.IsFredholm.isClosed_range
+ContinuousLinearMap.IsFredholm.isStrictMap
+ContinuousLinearMap.IsFredholm.mk
+ContinuousLinearMap.IsFredholm.nonempty_fredholmPackage
+ContinuousLinearMap.IsFredholm.of_isInvertible_restrict
+ContinuousLinearMap.IsFredholm.rec
+ContinuousLinearMap.IsFredholm.recOn
+ContinuousLinearMap.isFredholm_congr
+ContinuousLinearMap.isFredholm_iff_exists_isQuasiInverse
+ContinuousLinearMap.isFredholm_tfae
+ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_eqOn
+ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid
+ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient
+ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict
+ContinuousLinearMap.restrict.congr_simp
+FredholmDecomposition
+FredholmDecomposition.X₀
+FredholmDecomposition.X₁
+FredholmDecomposition.casesOn
+FredholmDecomposition.ctorIdx
+FredholmDecomposition.finite_X₀
+FredholmDecomposition.isTopCompl
+FredholmDecomposition.mk
+FredholmDecomposition.mk.inj
+FredholmDecomposition.mk.injEq
+FredholmDecomposition.mk.noConfusion
+FredholmDecomposition.mk.sizeOf_spec
+FredholmDecomposition.noConfusion
+FredholmDecomposition.noConfusionType
+FredholmDecomposition.proj
+FredholmDecomposition.rec
+FredholmDecomposition.recOn
+LinearMap.eqOn_eqLocus
+LinearMap.isClosed_range_of_isClosed_map_of_finiteDimensional_quotient
+LinearMap.isStrictMap_iff_isEmbedding_liftQ_ker
+LinearMap.isStrictMap_iff_isHomeomorph_quotKerEquivRange
+LinearMap.isStrictMap_iff_isOpenQuotientMap_rangeRestrict
+LinearMap.isStrictMap_prodMap
+LinearMap.isStrictMap_prodMap_iff
+Submodule.isFredholm_subtypeL
+Submodule.mkQL_isFredholmStruct
+Submodule.quotientEquivOfIsTopCompl.congr_simp
+Topology.IsClosedEmbedding.isFredholmStruct
+Topology.IsQuotientMap.isFredholm

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
5010	2	exposed public sections

Current commit f4b8767841
Reference commit 0c00cfd56d

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: composition of Fredholm operators #41601
  By Dependent Issues (🤖). Happy coding!