[Merged by Bors] - feat: dot notation for IsTheta.add_isLittleO, and add_commed variants

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -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₁) :=
+  add_comm f₁ f₂ ▸ h.right_isBigO_add
+
 /-- If `f x = O(g x)` along `cofinite`, then there exists a positive constant `C` such that
 `‖f x‖ ≤ C * ‖g x‖` whenever `g x ≠ 0`. -/
 theorem bound_of_isBigO_cofinite (h : f =O[cofinite] g'') :

Mathlib/Analysis/Asymptotics/Theta.lean

@@ -325,8 +325,20 @@ alias ⟨IsTheta.of_const_mul_right, IsTheta.const_mul_right⟩ := isTheta_const
 #align asymptotics.is_Theta.of_const_mul_right Asymptotics.IsTheta.of_const_mul_right
 #align asymptotics.is_Theta.const_mul_right Asymptotics.IsTheta.const_mul_right
 
-lemma IsTheta.add_isLittleO {f₁ f₂ : α → E'}
-    (h : f₂ =o[l] f₁) : (f₁ + f₂) =Θ[l] f₁ :=
-  ⟨(isBigO_refl _ _).add_isLittleO h, by rw [add_comm]; exact h.right_isBigO_add⟩
+theorem IsLittleO.right_isTheta_add {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :
+    f₂ =Θ[l] (f₁ + f₂) :=
+  ⟨h.right_isBigO_add, h.add_isBigO (isBigO_refl _ _)⟩
+
+theorem IsLittleO.right_isTheta_add' {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :
+    f₂ =Θ[l] (f₂ + f₁) :=
+  add_comm f₁ f₂ ▸ h.right_isTheta_add
+
+lemma IsTheta.add_isLittleO {f₁ f₂ : α → E'} {g : α → F}
+    (hΘ : f₁ =Θ[l] g) (ho : f₂ =o[l] g) : (f₁ + f₂) =Θ[l] g :=
+  (ho.trans_isTheta hΘ.symm).right_isTheta_add'.symm.trans hΘ
+
+lemma IsLittleO.add_isTheta {f₁ f₂ : α → E'} {g : α → F}
+    (ho : f₁ =o[l] g) (hΘ : f₂ =Θ[l] g) : (f₁ + f₂) =Θ[l] g :=
+  add_comm f₁ f₂ ▸ hΘ.add_isLittleO ho
 
 end Asymptotics