internlm/Lean-Github huggingface dataset:
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (Nat.succ m • g) - ↑(Nat.succ m) * f g| ≤ bound * (|↑(Nat.succ m)| + 1)
Tactic:
rewrite [show m.succ • g = g + m • g from AddMonoid.nsmul_succ ..,
         show ↑(m.succ) * f g = f g + m * f g
           by rewrite [Nat.succ_eq_add_one, Nat.cast_succ]; linarith]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (g + m • g) - (f g + ↑m * f g)| ≤ bound * (|↑(Nat.succ m)| + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (g + m • g) - (f g + ↑m * f g)| ≤ bound * (|↑(Nat.succ m)| + 1)
Tactic:
calc |f (g + m • g) - (f g + m * f g)|
    = |(f (g + m • g) - f g - f (m • g)) + (f (m • g) - m * f g)|
        := congrArg Int.natAbs <| by linarith
  _ ≤ |f (g + m • g) - f g - f (m • g)| + |f (m • g) - m * f g|
        := Int.natAbs_add_le ..
  _ ≤ bound + bound * (m + 1)
        := Nat.add_le_add (h.almost_additive ..) hᵢ
  _ = bound * (m.succ + 1)
        := by linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ ↑(Nat.succ m) * f g = f g + ↑m * f g
Tactic:
rewrite [Nat.succ_eq_add_one, Nat.cast_succ]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ (↑m + 1) * f g = f g + ↑m * f g
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ (↑m + 1) * f g = f g + ↑m * f g
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ f (g + m • g) - (f g + ↑m * f g) = f (g + m • g) - f g - f (m • g) + (f (m • g) - ↑m * f g)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ bound + bound * (m + 1) = bound * (Nat.succ m + 1)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)
Tactic:
rewrite [show Int.negSucc Nat.zero = -1 by rfl]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (-1 • g) - -1 * f g| ≤ bound * (|-1| + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (-1 • g) - -1 * f g| ≤ bound * (|-1| + 1)
Tactic:
simpa using h.almost_neg g
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ Int.negSucc Nat.zero = -1
Tactic:
rfl
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc (Nat.succ m) • g) - Int.negSucc (Nat.succ m) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
conv => lhs; rewrite [←Int.negSucc_sub_one]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f ((Int.negSucc m - 1) • g) - (Int.negSucc m - 1) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f ((Int.negSucc m - 1) • g) - (Int.negSucc m - 1) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
rewrite [sub_zsmul, one_zsmul, sub_mul, one_mul]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
calc |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)|
    = |(-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g))
       + (f (Int.negSucc m • g) - Int.negSucc m * f g)|
        := congrArg Int.natAbs <| by linarith
  _ ≤ |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g|
      + |f (Int.negSucc m • g) - Int.negSucc m * f g|
        := by conv => rhs; arg 1; rewrite [←Int.natAbs_neg]
              apply Int.natAbs_add_le
  _ ≤ bound + bound * (|Int.negSucc m| + 1)
        := Nat.add_le_add (by rewrite [←congrArg f <| neg_add_cancel_right ..]
                              apply h.almost_additive _ g)
                          hᵢ
  _ = bound * (|Int.negSucc m.succ| + 1)
        := by simp only [Int.natAbs_negSucc]; linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g) =
    -(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)| ≤
    |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g| + |f (Int.negSucc m • g) - Int.negSucc m * f g|
Tactic:
conv => rhs; arg 1; rewrite [←Int.natAbs_neg]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)| ≤
    |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g)| + |f (Int.negSucc m • g) - Int.negSucc m * f g|
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)| ≤
    |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g)| + |f (Int.negSucc m • g) - Int.negSucc m * f g|
Tactic:
apply Int.natAbs_add_le
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g| ≤ bound
Tactic:
rewrite [←congrArg f <| neg_add_cancel_right ..]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -?m.60523 + ?m.60523) - f (Int.negSucc m • g + -g) - f g| ≤ bound

G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ G
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -?m.60523 + ?m.60523) - f (Int.negSucc m • g + -g) - f g| ≤ bound

G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ G
Tactic:
apply h.almost_additive _ g
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ bound + bound * (|Int.negSucc m| + 1) = bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
simp only [Int.natAbs_negSucc]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ bound + bound * (Nat.succ m + 1) = bound * (Nat.succ (Nat.succ m) + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ bound + bound * (Nat.succ m + 1) = bound * (Nat.succ (Nat.succ m) + 1)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul_interchange
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f ((m * n) • g) - n * f (m • g)| + |f ((m * n) • g) - m * f (n • g)| =
    |f (n • m • g) - n * f (m • g)| + |f (m • n • g) - m * f (n • g)|
Tactic:
congr 3
Proof state after:
case e_a.e_m.e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f ((m * n) • g) = f (n • m • g)

case e_a.e_m.e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f ((m * n) • g) = f (m • n • g)
Theorem: AlmostAdditive.almost_smul_interchange
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (n • m • g) - n * f (m • g)| + |f (m • n • g) - m * f (n • g)| ≤ bound * (|n| + 1) + bound * (|m| + 1)
Tactic:
apply Nat.add_le_add <;> apply h.almost_smul
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul_interchange
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ bound * (|n| + 1) + bound * (|m| + 1) = bound * (|m| + |n| + 2)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul_interchange_int
Proof state before:
G : Type ?u.71849
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m✝ n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
⊢ |n * f m - m * f n| ≤ bound * (|m| + |n| + 2)
Tactic:
lax_exact h.almost_smul_interchange m n 1 <;> rw [zsmul_int_one]
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_upper_bound
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (n • g)| ≤ |f (n • g) - n * f g| + |n * f g|
Tactic:
lax_exact Int.natAbs_add_le (f (n • g) - n * f g) (n * f g)
Proof 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
⊢ f (n • g) = f (n • g) - n * f g + n * f g
Theorem: AlmostAdditive.linear_growth_upper_bound
Proof 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
⊢ f (n • g) = f (n • g) - n * f g + n * f g
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_upper_bound
Proof 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| + |n * f g| ≤ (bound + |f g|) * |n| + bound
Tactic:
linarith [h.almost_smul n g, Int.natAbs_mul n (f g)]
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_upper_bound_int
Proof state before:
G : Type ?u.78830
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ |f n| ≤ (bound + |f 1|) * |n| + bound
Tactic:
lax_exact h.linear_growth_upper_bound n 1
Proof state after:
case e_a.e_m.e_a
G : Type ?u.78830
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1
Theorem: AlmostAdditive.linear_growth_upper_bound_int
Proof state before:
case e_a.e_m.e_a
G : Type ?u.78830
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1
Tactic:
rw [zsmul_int_one]
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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]
Proof 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)|
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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
Proof 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|
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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]
Proof 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)|
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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]
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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]
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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))
Proof 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)
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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
Proof 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|
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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]
Proof 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|
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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
Proof 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
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_lower_bound
Proof 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]
Proof state after:
no goals
Theorem: AlmostAdditive.linear_growth_lower_bound_int
Proof state before:
G : Type ?u.87514
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ (|f 1| - bound) * |n| - bound ≤ |f n|
Tactic:
lax_exact h.linear_growth_lower_bound n 1
Proof state after:
case e_a.e_m.e_a
G : Type ?u.87514
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1
Theorem: AlmostAdditive.linear_growth_lower_bound_int
Proof state before:
case e_a.e_m.e_a
G : Type ?u.87514
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1
Tactic:
rw [zsmul_int_one]
Proof state after:
no goals
Theorem: AlmostAdditive.add
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ f₁ (x + y) + f₂ (x + y) - (f₁ x + f₂ x) - (f₁ y + f₂ y) = f₁ (x + y) - f₁ x - f₁ y + (f₂ (x + y) - f₂ x - f₂ y)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.add
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (x + y) - f₁ x - f₁ y + (f₂ (x + y) - f₂ x - f₂ y)| ≤ bound₁ + bound₂
Tactic:
transitivity
Proof state after:
case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (x + y) - f₁ x - f₁ y + (f₂ (x + y) - f₂ x - f₂ y)| ≤ ?m

case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ ?m ≤ bound₁ + bound₂

case m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ ℕ
Theorem: AlmostAdditive.neg
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |-f (x + y) - -f x - -f y| = |-(-f (x + y) - -f x - -f y)|
Tactic:
rw [Int.natAbs_neg]
Proof state after:
no goals
Theorem: AlmostAdditive.neg
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ -(-f (x + y) - -f x - -f y) = f (x + y) - f x - f y
Tactic:
linarith
Proof state after:
no goals
Theorem: Bounded.of_bddAbove_of_bddBelow
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
⊢ Bounded f (max |boundᵤ| |boundₗ|)
Tactic:
intro g
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ |f g| ≤ max |boundᵤ| |boundₗ|
Theorem: Bounded.of_bddAbove_of_bddBelow
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ |f g| ≤ max |boundᵤ| |boundₗ|
Tactic:
apply Int.natAbs_le <;> custom_zify
Proof state after:
case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ f g ≤ max ↑(|boundᵤ|) ↑(|boundₗ|)

case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ -f g ≤ max ↑(|boundᵤ|) ↑(|boundₗ|)
Theorem: Bounded.bddAbove
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : Bounded f bound
g : G
⊢ ↑(|f g|) ≤ ↑bound
Tactic:
exact_mod_cast h g
Proof state after:
no goals
Theorem: Bounded.bddBelow
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : Bounded f bound
g : G
⊢ ↑(|f g|) ≤ ↑bound
Tactic:
exact_mod_cast h g
Proof state after:
no goals
Theorem: Bounded.Bounded.almost_additive
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : Bounded f bound
g₁ g₂ : G
⊢ |f (g₁ + g₂)| + |-f g₁| + |-f g₂| ≤ bound * 3
Tactic:
linarith [(f g₁).natAbs_neg, (f g₂).natAbs_neg,
          h (g₁ + g₂), h g₁, h g₂]
Proof state after:
no goals