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: dot notation for IsTheta.add_isLittleO
, and add_comm
ed variants
#10386
Conversation
…iants BREAKING CHANGE: Change `IsTheta.add_isLittleO` into a dot-notation statement, in line with the existing `IsBigO`. Move the current `IsTheta.add_isLittleO` statement to `IsLittleO.left_isTheta_add`, in line with the existing `IsLittleO.left_isIsBigO_add`. feat: Add `add_comm`ed variants of related lemmas. These changes smoothen the flow when proving e.g. `a + b + c + d + e + f =Θ[l] d`.
3c049e4
to
d60ead1
Compare
@@ -2137,6 +2137,10 @@ theorem IsLittleO.right_isBigO_add {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) | |||
((h.def' one_half_pos).right_le_add_of_lt_one one_half_lt_one).isBigO | |||
#align asymptotics.is_o.right_is_O_add Asymptotics.IsLittleO.right_isBigO_add | |||
|
|||
theorem IsLittleO.right_isBigO_add' {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : | |||
f₂ =O[l] (f₂ + f₁) := | |||
Trans.trans h.right_isBigO_add (add_comm _ _) |
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.
Does this work? Untested...
Trans.trans h.right_isBigO_add (add_comm _ _) | |
h.right_isBigO_add.trans (add_comm _ _) |
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.
Unfortunately not, since this is IsBigO
trans Eq
, whereas IsBigO.trans
is IsBigO
trans IsBigO
. There is also no IsBigO.trans_eq
lemma; instead there is this instance for Trans.trans
: https://github.com/leanprover/lean4/blob/56d703db8eec777b813a198e2126115bda9d3a9b/src/Init/Prelude.lean#L1152-L1153
EDIT: I can, however, copy from the linked proof: add_comm f₁ f₂ ▸ h.right_isBigO_add
|
||
theorem IsLittleO.right_isTheta_add' {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : | ||
f₂ =Θ[l] (f₂ + f₁) := | ||
Trans.trans h.right_isTheta_add (add_comm _ _) |
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.
Idem
Trans.trans h.right_isTheta_add (add_comm _ _) | |
h.right_isTheta_add.trans (add_comm _ _) |
I'm not a big fan of using |
👍 I'll wait for ideas here. It might involve renaming both this new |
IsTheta.add_isLittleO
, and add_comm
ed variantsIsTheta.add_isLittleO
, and add_comm
ed variants
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.
This looks good to me!
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.
Thanks 🎉
bors merge
…ants (#10386) BREAKING CHANGE: Change `IsTheta.add_isLittleO` into a dot-notation statement, in line with the existing `IsBigO.add_isLittleO`. Move the current `IsTheta.add_isLittleO` statement to `IsLittleO.right_isTheta_add'`, in line with the existing `IsLittleO.right_isBigO_add`. feat: Add `add_comm`ed variants of related lemmas. These changes smoothen the flow when proving e.g. `a + b + c + d + e + f =Θ[l] d`. Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
Pull request successfully merged into master. Build succeeded: |
IsTheta.add_isLittleO
, and add_comm
ed variantsIsTheta.add_isLittleO
, and add_comm
ed variants
…ants (#10386) BREAKING CHANGE: Change `IsTheta.add_isLittleO` into a dot-notation statement, in line with the existing `IsBigO.add_isLittleO`. Move the current `IsTheta.add_isLittleO` statement to `IsLittleO.right_isTheta_add'`, in line with the existing `IsLittleO.right_isBigO_add`. feat: Add `add_comm`ed variants of related lemmas. These changes smoothen the flow when proving e.g. `a + b + c + d + e + f =Θ[l] d`. Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
…ants (#10386) BREAKING CHANGE: Change `IsTheta.add_isLittleO` into a dot-notation statement, in line with the existing `IsBigO.add_isLittleO`. Move the current `IsTheta.add_isLittleO` statement to `IsLittleO.right_isTheta_add'`, in line with the existing `IsLittleO.right_isBigO_add`. feat: Add `add_comm`ed variants of related lemmas. These changes smoothen the flow when proving e.g. `a + b + c + d + e + f =Θ[l] d`. Co-authored-by: L Lllvvuu <git@llllvvuu.dev>
BREAKING CHANGE: Change
IsTheta.add_isLittleO
into a dot-notation statement, in line with the existingIsBigO.add_isLittleO
. Move the currentIsTheta.add_isLittleO
statement toIsLittleO.right_isTheta_add'
, in line with the existingIsLittleO.right_isBigO_add
.feat: Add
add_comm
ed variants of related lemmas.These changes smoothen the flow when proving e.g.
a + b + c + d + e + f =Θ[l] d
.