Theorem: AlmostAdditive.linear_growth_lower_bound (RealsQuasiMorphisms/Basic.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ (|f g| - bound) * |n| - bound ≤ |f (n • g)|
Tactic:
rewrite [tsub_mul, Nat.sub_sub, ←Nat.mul_succ]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| - bound * Nat.succ |n| ≤ |f (n • g)|

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| - bound * Nat.succ |n| ≤ |f (n • g)|
Tactic:
apply Nat.sub_le_of_le_add
State after:
case h
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| ≤ |f (n • g)| + bound * Nat.succ |n|

State before:
case h
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| ≤ |f (n • g)| + bound * Nat.succ |n|
Tactic:
rewrite [Nat.add_comm]
State after:
case h
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| ≤ bound * Nat.succ |n| + |f (n • g)|

State before:
case h
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| ≤ bound * Nat.succ |n| + |f (n • g)|
Tactic:
calc |f g| * |n|
  = |n * f g|                       := by rw [Nat.mul_comm, Int.natAbs_mul]
_ ≤ |n * f g - f (n • g)| + |f (n • g)|
      := by lax_exact Int.natAbs_add_le (n * f g - f (n • g)) (f (n • g)); linarith
_ = |f (n • g) - n * f g| + |f (n • g)|
      := by congr 1; rewrite [←Int.natAbs_neg]
            congr 1; linarith
_ ≤ bound * (|n| + 1) + |f (n • g)| := by linarith [h.almost_smul n g]
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f g| * |n| = |n * f g|
Tactic:
rw [Nat.mul_comm, Int.natAbs_mul]
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |n * f g| ≤ |n * f g - f (n • g)| + |f (n • g)|
Tactic:
lax_exact Int.natAbs_add_le (n * f g - f (n • g)) (f (n • g))
State after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ n * f g = n * f g - f (n • g) + f (n • g)

State before:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ n * f g = n * f g - f (n • g) + f (n • g)
Tactic:
linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |n * f g - f (n • g)| + |f (n • g)| = |f (n • g) - n * f g| + |f (n • g)|
Tactic:
congr 1
State after:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |n * f g - f (n • g)| = |f (n • g) - n * f g|

State before:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |n * f g - f (n • g)| = |f (n • g) - n * f g|
Tactic:
rewrite [←Int.natAbs_neg]
State after:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |-(n * f g - f (n • g))| = |f (n • g) - n * f g|

State before:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |-(n * f g - f (n • g))| = |f (n • g) - n * f g|
Tactic:
congr 1
State after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ -(n * f g - f (n • g)) = f (n • g) - n * f g

State before:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ -(n * f g - f (n • g)) = f (n • g) - n * f g
Tactic:
linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (n • g) - n * f g| + |f (n • g)| ≤ bound * (|n| + 1) + |f (n • g)|
Tactic:
linarith [h.almost_smul n g]
State after:
no goals