feat(Analysis/Calculus/AddTorsor/AffineMap): smoothness of AffineMap.lineMap#39206
Open
FordUniver wants to merge 1 commit into
Open
feat(Analysis/Calculus/AddTorsor/AffineMap): smoothness of AffineMap.lineMap#39206FordUniver wants to merge 1 commit into
FordUniver wants to merge 1 commit into
Conversation
…lineMap Add `AffineMap.lineMap_contDiff_uncurry` (joint smoothness in all three arguments), `AffineMap.lineMap_contDiff` (smoothness in the parameter with fixed endpoints), and the composition family `ContDiff.lineMap`, `ContDiffOn.lineMap`, `ContDiffAt.lineMap`, `ContDiffWithinAt.lineMap`, mirroring the corresponding `Continuous` family in `Mathlib.Topology.Algebra.Affine`. The uncurried and `ContDiffWithinAt` forms are tagged `@[fun_prop]`. Closes the long-standing TODO at `MeasureTheory.Integral.CurveIntegral.Poincare:333` (`-- TODO: add ContDiff.lineMap etc`), where the absence of this API forced a manual `simp only [AffineMap.lineMap_apply_module]` unfold before `fun_prop` could close the goal. The Poincare proof now closes with just `fun_prop` once the new file is imported.
PR summary d59f7b3264
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare | 2440 | 2441 | +1 (+0.04%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare |
1 |
Declarations diff
+ ContDiff.lineMap
+ ContDiffAt.lineMap
+ ContDiffOn.lineMap
+ ContDiffWithinAt.lineMap
+ lineMap_contDiff
+ lineMap_contDiff_uncurry
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.
No changes to strong technical debt.
No changes to weak technical debt.
github-actions
Bot
added
the
t-measure-probability
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add
AffineMap.lineMap_contDiff_uncurry(joint smoothness in all three arguments),AffineMap.lineMap_contDiff(smoothness in the parameter with fixed endpoints), and the composition familyContDiff.lineMap,ContDiffOn.lineMap,ContDiffAt.lineMap,ContDiffWithinAt.lineMap, mirroring the correspondingContinuousfamily inMathlib.Topology.Algebra.Affine. The uncurried andContDiffWithinAtforms are tagged@[fun_prop]so the rest are automatically derivable. Closes the TODO atMathlib.MeasureTheory.Integral.CurveIntegral.Poincare:333where the proof now reduces tofun_prop.Came up while formalizing the descent lemma for Lipschitz-smooth functions, where
Path.segment a bbeing smooth on the unit interval is needed to apply FTC along the segment;AffineMap.lineMap_contDiffis the lemma directly used there. Two things I was genuinely not quite sure about:Should the three convenience variants
ContDiffAt.lineMap,ContDiffOn.lineMap, andContDiff.lineMapbe included? They are not strictly necessary but they exist for users wanting to writeh₁.lineMap h₂ hgin dot notation by hand, and they mirror the convention of theContinuous.lineMapfamily.Is
Mathlib.Analysis.Calculus.AddTorsor.AffineMapthe right home, and is addingpublic import Mathlib.Analysis.Calculus.AddTorsor.AffineMaptoPoincare.leanto close the TODO reasonable? The placement mirrors theContinuous.lineMapfamily inMathlib.Topology.Algebra.Affine, but hiding a@[fun_prop]in a file at the bottom of the hierarchy and needing to import it feels a bit off.