feat(Manifold/Instances/Icc): golf smoothness proof using immersions#29077
feat(Manifold/Instances/Icc): golf smoothness proof using immersions#29077grunweg wants to merge 52 commits intoleanprover-community:masterfrom
Conversation
The old name did not follow the naming convention; when adding restrOpen in the next commit, the distinction starts to matter.
These are analogues to existing lemmas about subtypeRestr, but I want to use .restr (not .subtypeRestr).
if e is in the maximal atlas, so is e.restr s for any open set s.
…maining) Apart from that, everything is sorry-free
This version was missing, we only had the withinAt version.
Continuity remains (warm-up), and three small computations
At best, "is locally an embedding" would work... but need to make that precise (and AFAICT, there's no such notion in mathlib yet). For now, .continuousOn is the closest approximation I have..."
doesn't quite work yet
Perhaps half done, ask on zulip about good design ideas!
Works, but need more focused time
Except for fiddling with my chosen charts, everything works.
PR summary cefe7b7756
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Geometry.Manifold.Instances.Icc | 2147 | 2152 | +5 (+0.23%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Geometry.Manifold.Riemannian.Basic |
1 |
Mathlib.Geometry.Manifold.Riemannian.PathELength |
2 |
Mathlib.Geometry.Manifold.Instances.Icc |
5 |
Mathlib.Geometry.Manifold.IsImmersionEmbedding (new file) |
2067 |
Declarations diff
+ ContDiffWithinAt.congr'
+ ContMDiffAt.iff_comp_isImmersionAt
+ Continuous.of_comp_iff_isInducing_restr
+ IsEmbedding.subtype_map_of_subset
+ IsImmersion
+ IsImmersionAt
+ StructureGroupoid.subtypeRestr_mem_maximalAtlas
+ _root_.ContMDiff.iff_comp_isImmersion
+ _root_.Set.EqOn.prodMap
+ aux1
+ aux2
+ bar
+ bar_apply
+ bars
+ barz
+ codChart
+ codChart_mem_maximalAtlas
+ congr
+ congr_of_eventuallyEq
+ contDiffAt_prod_iff
+ contDiffOn_prod_iff
+ contDiff_prod_iff
+ contMDiff
+ contMDiffAt
+ contMDiffAt_iff_of_mem_maximalAtlas
+ contMDiffAt_writtenInExtend_iff
+ contMDiffOn_extend
+ contMDiffWithinAt_writtenInExtend_iff
+ contMDiff_iff_comp_subtype_coe_Icc
+ continuousAt
+ continuousAt_iff_comp_isImmersionAt
+ domChart
+ domChart_mem_maximalAtlas
+ eqOn_domChart_source
+ equiv
+ exists_nbhd_restr_isEmbedding
+ extend_prod
+ extend_target_eq_image_source
+ foo
+ isClosedEmbedding_symm_restrict
+ isEmbedding_extend_restrict
+ isEmbedding_extend_symm_restrict
+ isEmbedding_symm_restrict
+ isImmersionAt
+ isImmersion_subtype_coe_Icc
+ map_source_subset_source
+ map_target_subset_target
+ mem_codChart_source
+ mem_domChart_source
+ mem_maximalAtlas_prod
+ mk_of_continuousAt
+ nhds_eq_comap
+ prod_symm_trans_prod
+ restr_eqOnSource_restr
+ restr_inter_source
+ restr_mem_maximalAtlas
+ restr_mem_maximalAtlas_aux1
+ restr_mem_maximalAtlas_aux2
+ restr_symm_trans
+ rightInverse_restrict
+ symm_trans_restr
+ writtenInCharts
++ aux
++ contMDiffOn_writtenInExtend_iff
++ prodMap
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.
Increase in tech debt: (relative, absolute) = (3.00, 0.75)
| Current number | Change | Type |
|---|---|---|
| 4 | 3 | large files |
Current commit 54b6719c7e
Reference commit cefe7b7756
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
This PR/issue depends on:
|
|
This pull request has conflicts, please merge |
Prove that the inclusion of an interval into the real numbers is a smooth immersion,
and use this to golf the proof that this inclusion is smooth.
TODO: right now, the computation doesn't check out; I need to tweak the charts I have. But that is surely doable.
A future PR will prove it is a smooth embedding.