[Merged by Bors] - feat: more results about IsLittleOTVS#20220
[Merged by Bors] - feat: more results about IsLittleOTVS#20220eric-wieser wants to merge 18 commits intomasterfrom
IsLittleOTVS#20220Conversation
PR summary 345e7aba40Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
IsLittleOTVS.monoIsLittleOTVS.mono and IsLittleOTVS.sup
IsLittleOTVS.mono and IsLittleOTVS.sup IsLittleOTVS.{mono,sup,insert}
IsLittleOTVS.{mono,sup,insert} IsLittleOTVS
This makes it easier to copy over API from `IsLittleO`. This also changes the argument order to be consistent with `IsLittleO`.
|
This PR/issue depends on:
|
| h.congr hf fun _ => rfl | ||
|
|
||
| theorem IsLittleOTVS.congr_right (h : f =o[𝕜;l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =o[𝕜;l] g₂ := | ||
| h.congr (fun _ => rfl) hg |
There was a problem hiding this comment.
I'm not sure that we need these non-filter congr lemmas. Should we use EventuallyEq everywhere?
There was a problem hiding this comment.
These are copied from the IsLittleO ones. Let's either deprecate them there first, or deprecate both later.
| _ ≤ δ * egauge 𝕜 (ball 0 1) (g x) := by gcongr; apply le_egauge_ball_one | ||
|
|
||
| alias ⟨isLittleOTVS.isLittleO, IsLittle.isLittleOTVS⟩ := isLittleOTVS_iff_isLittleO | ||
| alias ⟨isLittleOTVS.isLittleO, IsLittleO.isLittleOTVS⟩ := isLittleOTVS_iff_isLittleO |
There was a problem hiding this comment.
Do we need a deprecated alias here?
There was a problem hiding this comment.
No, I think we can get away with it.
| nonrec theorem HasFDerivAtFilter.mono (h : HasFDerivAtFilter f f' x L₂) (hst : L₁ ≤ L₂) : | ||
| HasFDerivAtFilter f f' x L₁ := | ||
| .of_isLittleO <| h.isLittleO.mono hst | ||
| .of_isLittleOTVS <| h.isLittleOTVS.mono hst |
There was a problem hiding this comment.
Should we change typeclass assumptions here, or do you want to do it in another PR (e.g., wait until we can generalize more theorems)?
There was a problem hiding this comment.
In another PR; I want to generalize as much as possible without having to shuffle things around and make the diff hard to process.
| mem_prod_self_iff.trans <| by simp only [prod_subset_iff, mem_setOf_eq] | ||
|
|
||
| /-- A version of `eventually_prod_self_iff` that is more suitable for forward rewriting. -/ | ||
| lemma eventually_prod_self_iff' {r : α × α → Prop} : |
There was a problem hiding this comment.
Note that this lemma is no longer used in this PR.
There was a problem hiding this comment.
I think it's still a nice one to have, and in general we have these two variants for theorems about quantifiers.
|
I'm happy with this PR (modulo a few comments above), but I pushed some code here, so we need a review from another maintainer. |
|
maintainer delegate |
|
🚀 Pull request has been placed on the maintainer queue by urkud. |
ocfnash
left a comment
There was a problem hiding this comment.
One question about naming but LGTM, thanks!
bors merge
| gcongr | ||
|
|
||
| theorem isLittleOTVS_iff_smallSets : | ||
| f =o[𝕜; l] g ↔ ∀ U ∈ 𝓝 0, ∀ᶠ V in (𝓝 0).smallSets, ∀ ε ≠ (0 : ℝ≥0), |
There was a problem hiding this comment.
Just a remark that I'd rather that what is called ε here was instead C or really anything other than ε (or δ) as this constant will generally be large.
I note that you're being consistent with the definition IsLittleOTVS so I guess I'm asking how you would feel about following up with a renaming PR to rename the constant there?
It will be cleaner to generalize the results for `fderiv` after writing a few more of these lemmas, rather than shuffling everything around. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
|
Pull request successfully merged into master. Build succeeded: |
IsLittleOTVSIsLittleOTVS
It will be cleaner to generalize the results for
fderivafter writing a few more of these lemmas, rather than shuffling everything around.f =o[𝕜;l] gnotation forIsLittleOTVS#20305