English
If the weighted orders of f and g are distinct, the weighted order of f+g is the infimum of the two.
Русский
Если взвешенные порядки f и g различны, то взвешенный порядок f+g равен inf(ω_w(f), ω_w(g)).
LaTeX
$$weightedOrder w (f+g) = min (weightedOrder w f) (weightedOrder w g) if weightedOrder w f ≠ weightedOrder w g$$
Lean4
/-- The weighted_order of the sum of two formal power series
is the minimum of their orders if their orders differ. -/
theorem weightedOrder_add_of_weightedOrder_ne (h : f.weightedOrder w ≠ g.weightedOrder w) :
weightedOrder w (f + g) = weightedOrder w f ⊓ weightedOrder w g :=
by
refine le_antisymm ?_ (min_weightedOrder_le_add w)
wlog H₁ : f.weightedOrder w < g.weightedOrder w
· rw [add_comm f g, inf_comm]
exact this _ h.symm ((le_of_not_gt H₁).lt_of_ne' h)
simp only [le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₁]
exact ⟨le_rfl, le_of_lt H₁⟩
