New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(analysis/asymptotics/asymptotics): generalize, golf #15010
Conversation
This PR/issue depends on: |
@@ -143,10 +143,14 @@ theorem is_o.is_O (hgf : f =o[l] g) : f =O[l] g := hgf.is_O_with.is_O | |||
|
|||
lemma is_O.is_O_with : f =O[l] g → ∃ c : ℝ, is_O_with c l f g := is_O_iff_is_O_with.1 | |||
|
|||
theorem is_O_with.weaken' (h : is_O_with c l f g) (hg : ∀ᶠ x in l, 0 ≤ ∥g x∥) (hc : c ≤ c') : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't understand the point of stating things assuming only has_norm
and assumptions saying some norms are non negative.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I left one result of this kind and renamed it to *_aux
. It is used to prove two versions of a lemma assuming has_norm
/semi_normed_group
for different types.
bors merge |
* add `is_o_iff_nat_mul_le`, `is_o_iff_nat_mul_le'`, `is_o_irrefl`, `is_O.not_is_o`, `is_o.not_is_O`; * generalize lemmas about `1 = o(f)`, `1 = O(f)`, `f = o(1)`, `f = O(1)` to `[has_one F] [norm_one_class F]`, add some `@[simp]` attrs; * rename `is_O_one_of_tendsto` to `filter.tendsto.is_O_one`; * golf some proofs
Pull request successfully merged into master. Build succeeded: |
* add `is_o_iff_nat_mul_le`, `is_o_iff_nat_mul_le'`, `is_o_irrefl`, `is_O.not_is_o`, `is_o.not_is_O`; * generalize lemmas about `1 = o(f)`, `1 = O(f)`, `f = o(1)`, `f = O(1)` to `[has_one F] [norm_one_class F]`, add some `@[simp]` attrs; * rename `is_O_one_of_tendsto` to `filter.tendsto.is_O_one`; * golf some proofs
is_o_iff_nat_mul_le
,is_o_iff_nat_mul_le'
,is_o_irrefl
,is_O.not_is_o
,is_o.not_is_O
;1 = o(f)
,1 = O(f)
,f = o(1)
,f = O(1)
to[has_one F] [norm_one_class F]
, add some@[simp]
attrs;is_O_one_of_tendsto
tofilter.tendsto.is_O_one
;@[simp]
to `real.norm_eq_abs #15006