Theorem: AlmostHom.comp_almost_mul (RealsQuasiMorphisms/Ring.lean)

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
Tactic:
let ⟨a', b', hlin⟩ := linear_growth_upper_bound_int f₂
State after:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
Tactic:
let ⟨b₁, hf₁⟩ := f₁.almostAdditive
State after:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
Tactic:
exact ⟨_, by
  intro n
  have hypcomm := AlmostAdditive.almost_smul_interchange (hf₁) (f₂ n) n 1
  specialize hlin n
  simp only [smul_eq_mul, mul_one] at hypcomm
  calc |n * (f₁.comp f₂ n) - f₂ n * f₁ n|
      ≤ b₁*(|f₂ n| + |n| + 2) := hypcomm
    _ ≤ b₁*(a'*|n| + b' + |n| + 2) :=
        by apply mul_le_mul_of_nonneg_left
            (by simp only [add_le_add_iff_right, hlin]) (zero_le _)
    _ = b₁*(|n| * (a' + 1) + (b'+ 2)) := by ring
    _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) :=
        by simp only [le_add_iff_nonneg_right, zero_le]
    _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) + b₁*(|n|)*(b'+2) :=
        by simp only [le_add_iff_nonneg_right, zero_le]
    _ = (|n|+1)*(b₁*(a'+1 + b'+2)) := by ring⟩
State after:
no goals

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
⊢ ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
intro n
State after:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
have hypcomm := AlmostAdditive.almost_smul_interchange (hf₁) (f₂ n) n 1
State after:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
specialize hlin n
State after:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
hlin : |toFun f₂ n| ≤ a' * |n| + b'
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
hlin : |toFun f₂ n| ≤ a' * |n| + b'
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
simp only [smul_eq_mul, mul_one] at hypcomm
State after:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
calc |n * (f₁.comp f₂ n) - f₂ n * f₁ n|
    ≤ b₁*(|f₂ n| + |n| + 2) := hypcomm
  _ ≤ b₁*(a'*|n| + b' + |n| + 2) :=
      by apply mul_le_mul_of_nonneg_left
          (by simp only [add_le_add_iff_right, hlin]) (zero_le _)
  _ = b₁*(|n| * (a' + 1) + (b'+ 2)) := by ring
  _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) :=
      by simp only [le_add_iff_nonneg_right, zero_le]
  _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) + b₁*(|n|)*(b'+2) :=
      by simp only [le_add_iff_nonneg_right, zero_le]
  _ = (|n|+1)*(b₁*(a'+1 + b'+2)) := by ring
State after:
no goals

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (|toFun f₂ n| + |n| + 2) ≤ b₁ * (a' * |n| + b' + |n| + 2)
Tactic:
apply mul_le_mul_of_nonneg_left
 (by simp only [add_le_add_iff_right, hlin]) (zero_le _)
State after:
no goals

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |toFun f₂ n| + |n| + 2 ≤ a' * |n| + b' + |n| + 2
Tactic:
simp only [add_le_add_iff_right, hlin]
State after:
no goals

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (a' * |n| + b' + |n| + 2) = b₁ * (|n| * (a' + 1) + (b' + 2))
Tactic:
ring
State after:
no goals

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (|n| * (a' + 1) + (b' + 2)) ≤ b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1)
Tactic:
simp only [le_add_iff_nonneg_right, zero_le]
State after:
no goals

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1) ≤
    b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1) + b₁ * |n| * (b' + 2)
Tactic:
simp only [le_add_iff_nonneg_right, zero_le]
State after:
no goals

State before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1) + b₁ * |n| * (b' + 2) = (|n| + 1) * (b₁ * (a' + 1 + b' + 2))
Tactic:
ring
State after:
no goals