Theorem: AlmostHom.positive_linear_growth_of_large_enough_value (RealsQuasiMorphisms/Order.lean)

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
⊢ ∀ (n : ℕ), ↑(|f (↑n * ↑m)|) ≥ (f ↑m - ↑bound) * ↑(|↑n|) - ↑bound
Tactic:
intro n
State after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (↑n * ↑m)|) ≥ (f ↑m - ↑bound) * ↑(|↑n|) - ↑bound

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (↑n * ↑m)|) ≥ (f ↑m - ↑bound) * ↑(|↑n|) - ↑bound
Tactic:
rewrite [←h_fm_nonneg, show (_:ℤ) * (m:ℤ) = (_:ℤ) • (m:ℤ) from rfl]
State after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (↑n • ↑m)|) ≥ (↑(|f ↑m|) - ↑bound) * ↑(|↑n|) - ↑bound

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (↑n • ↑m)|) ≥ (↑(|f ↑m|) - ↑bound) * ↑(|↑n|) - ↑bound
Tactic:
norm_cast
State after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat |f ↑m| bound * ↑n - ↑bound

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat |f ↑m| bound * ↑n - ↑bound
Tactic:
rewrite [Int.abs_eq_natAbs,
         Int.subNatNat_of_le <|
           show bound ≤ |f m| from Int.ofNat_le.mp <|
           calc (bound:ℤ) ≤ bound * 2 := by linarith
                        _ ≤ f m       := Int.le_of_lt h
                        _ ≤ |f m|     := Int.le_natAbs]
State after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ ↑(|f ↑m| - bound) * ↑n - ↑bound

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ ↑(|f ↑m| - bound) * ↑n - ↑bound
Tactic:
norm_cast
State after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ abs (f (n • ↑m)) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound
Tactic:
rewrite [Int.abs_eq_natAbs]
State after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑(|f (n • ↑m)|) ≥ Int.subNatNat ((|f ↑m| - bound) * n) bound
Tactic:
apply Int.le_trans (Int.subNatNat_le_sub ..)
State after:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑((|f ↑m| - bound) * n - bound) ≤ ↑(|f (n • ↑m)|)

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑((|f ↑m| - bound) * n - bound) ≤ ↑(|f (n • ↑m)|)
Tactic:
exact_mod_cast h_bound.linear_growth_lower_bound n m
State after:
no goals

State before:
G : Type ?u.55607
f : ℤ → ℤ
bound : ℕ
h_bound : AlmostAdditive f bound
m : ℕ
h : f ↑m > ↑bound * 2
h_fm_nonneg : ↑(|f ↑m|) = f ↑m
n : ℕ
⊢ ↑bound ≤ ↑bound * 2
Tactic:
linarith
State after:
no goals