Commit 2024-02-14 14:50 e1a19e31

View on Github →

feat: dot notation for IsTheta.add_isLittleO, and add_commed variants (#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_commed variants of related lemmas. These changes smoothen the flow when proving e.g. a + b + c + d + e + f =Θ[l] d.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.IsLittleO.right_isBigO_add'

Modified Mathlib/Analysis/Asymptotics/Theta.lean

added theorem Asymptotics.IsLittleO.add_isTheta

added theorem Asymptotics.IsLittleO.right_isTheta_add'

added theorem Asymptotics.IsLittleO.right_isTheta_add

modified theorem Asymptotics.IsTheta.add_isLittleO