feat: add mfderiv_const_smul#34262
feat: add mfderiv_const_smul#34262grunweg wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
|
@ocfnash Would you like to review a simple differential geometry PR again? If so, I have a solution for you. (And if no, I'll be happy to ask around instead.) |
PR summary 2050510330Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for Increase in tech debt: (relative, absolute) = (1.00, 0.00)
Current commit fee0f86a1e You can run this locally as
|
| lemma mfderiv_const_smul {x : M} (a : 𝕜) (v : TangentSpace I x) : | ||
| mfderiv I 𝓘(𝕜, E') (a • f) x v = a • mfderiv I 𝓘(𝕜, E') f x v := by | ||
| by_cases hs : MDifferentiableAt I 𝓘(𝕜, E') f x | ||
| · rw [const_smul_mfderiv hs]; rfl |
There was a problem hiding this comment.
The rfl here is suspicious. I briefly tried ContinuousLinearMap.smul_apply but it complains and erw? [ContinuousLinearMap.smul_apply] tells me:
❌️ at reducible transparency,
DFunLike.coe (β := fun x_1 ↦ TangentSpace 𝓘(𝕜, E') ((a • f) x))
and
DFunLike.coe (β := fun x_1 ↦ TangentSpace 𝓘(𝕜, E') (f x))
are not defeq, but they are at default transparency.Surely this sort of thing should just work?
There was a problem hiding this comment.
It should, but things appear less smooth. Floris and I were debugging this a bit last week. erw? has not helpful (as I just posted on zulip); it appears the issue is that the terms live in different tangent spaces. In this sense, const_smul_mfderiv is a bad lemma, because its left and right hand side live in different spaces.
This is a broader problem, let me start a thread on zulip.
| · by_cases ha : a = 0 | ||
| · have : a • f = 0 := by ext; simp [ha] | ||
| have aux : (fun _ ↦ 0 : M → E') = 0 := by rfl | ||
| rw [this, ha, ← aux] | ||
| simp | ||
| have hs' : ¬ MDifferentiableAt I 𝓘(𝕜, E') (a • f) x := | ||
| fun h ↦ hs (by simpa [ha] using h.const_smul a⁻¹) | ||
| rw [mfderiv_zero_of_not_mdifferentiableAt hs, mfderiv_zero_of_not_mdifferentiableAt hs'] | ||
| simp | ||
| rfl |
There was a problem hiding this comment.
Likewise here the rfls and the extent to which we need to work hard suggest to me that there is a bigger fish to fry with the API. Is it possible to get the below working smoothly?
| · by_cases ha : a = 0 | |
| · have : a • f = 0 := by ext; simp [ha] | |
| have aux : (fun _ ↦ 0 : M → E') = 0 := by rfl | |
| rw [this, ha, ← aux] | |
| simp | |
| have hs' : ¬ MDifferentiableAt I 𝓘(𝕜, E') (a • f) x := | |
| fun h ↦ hs (by simpa [ha] using h.const_smul a⁻¹) | |
| rw [mfderiv_zero_of_not_mdifferentiableAt hs, mfderiv_zero_of_not_mdifferentiableAt hs'] | |
| simp | |
| rfl | |
| · rcases eq_or_ne a 0 with rfl | ha; · simp; /- Should be finished now! -/ sorry | |
| have hs' : ¬ MDifferentiableAt I 𝓘(𝕜, E') (a • f) x := | |
| fun h ↦ hs (by simpa [ha] using h.const_smul a⁻¹) | |
| simp [mfderiv_zero_of_not_mdifferentiableAt hs, mfderiv_zero_of_not_mdifferentiableAt hs'] | |
| /- Should be finished now because of `ContinuousLinearMap.zero_apply`. -/ | |
| sorry |
There was a problem hiding this comment.
I've tried for a fair bit now: we may have missing API (there's no lemma mfderiv_zero, for instance) --- but we also have the same defeq problem above. Let me add that to the zulip thread.
There was a problem hiding this comment.
|
To be clear, I don't really care about golfing the proof but a proof like this suggests to me that we might need to tweak our upstream API since it shouldn't be this awkward. OTOH if these are known issues which we want to solve another time, we can move forward without addressing them here: clearly this lemma statement is good. |
|
This pull request has conflicts, please merge |
This generalises an existing mathlib lemma (as the differentiability hypothesis is in fact not necessary).
Co-authored-by: Patrick Massot patrickmassot@free.fr
Note: this PR is now lower-priority (after some reorgs it is no longer on the path to the Levi-Civita connection); it should be rewritten following the approach in #34263.