internlm/Lean-Github huggingface dataset:
Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ toFun f g ≤ ↑bound' - bound
Tactic:
have : f g - -f (-g) ≤ bound' := by
  apply Int.le_trans (Int.le_natAbs ..); apply Int.ofNat_le.mpr
  rewrite [show f g - -f (-g) = f (-g) - -f g by abel]; exact hₐ g
Proof state after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
this : toFun f g - -toFun f (-g) ≤ ↑bound'
⊢ toFun f g ≤ ↑bound' - bound
Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
this : toFun f g - -toFun f (-g) ≤ ↑bound'
⊢ toFun f g ≤ ↑bound' - bound
Tactic:
linarith [this, h (neg_nonneg_of_nonpos h_g)]
Proof state after:
no goals
Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ toFun f g - -toFun f (-g) ≤ ↑bound'
Tactic:
apply Int.le_trans (Int.le_natAbs ..)
Proof state after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ ↑(|toFun f g - -toFun f (-g)|) ≤ ↑bound'
Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ ↑(|toFun f g - -toFun f (-g)|) ≤ ↑bound'
Tactic:
apply Int.ofNat_le.mpr
Proof state after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f g - -toFun f (-g)| ≤ bound'
Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f g - -toFun f (-g)| ≤ bound'
Tactic:
rewrite [show f g - -f (-g) = f (-g) - -f g by abel]
Proof state after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f (-g) - -toFun f g| ≤ bound'
Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f (-g) - -toFun f g| ≤ bound'
Tactic:
exact hₐ g
Proof state after:
no goals
Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ toFun f g - -toFun f (-g) = toFun f (-g) - -toFun f g
Tactic:
abel
Proof state after:
no goals
Theorem: AlmostHom.nonneg_of_bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound
g : G
h_g : g ≥ 0
⊢ toFun f g ≥ -bound - ↑bound'
Tactic:
have : f (-g) - -f g ≥ -bound' := Int.neg_le_self_of_natAbs_le (hₐ g)
Proof state after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound
g : G
h_g : g ≥ 0
this : toFun f (-g) - -toFun f g ≥ -↑bound'
⊢ toFun f g ≥ -bound - ↑bound'
Theorem: AlmostHom.nonneg_of_bddAbove_on_nonpos
Proof state before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound
g : G
h_g : g ≥ 0
this : toFun f (-g) - -toFun f g ≥ -↑bound'
⊢ toFun f g ≥ -bound - ↑bound'
Tactic:
linarith [this, h (neg_nonpos_of_nonneg h_g)]
Proof state after:
no goals
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ |toFun f g| ≤ Int.toNat (max (max bound₁ bound₂) (max bound₃ bound₄))
Tactic:
custom_zify
Proof state after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ ↑(Int.toNat (max (max bound₁ bound₂) (max bound₃ bound₄)))
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ ↑(Int.toNat (max (max bound₁ bound₂) (max bound₃ bound₄)))
Tactic:
refine Int.le_trans ?_ (Int.self_le_toNat ..)
Proof state after:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
cases le_total 0 g
Proof state after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : 0 ≤ g
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)

case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : 0 ≤ g
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)

case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
case' inl h_ge =>
  specialize h₁' h_ge; specialize h₂' h_ge
  refine Int.le_trans ?_ (Int.le_max_left ..)
Proof state after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂

case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂

case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
case' inr h_le =>
  specialize h₃' h_le; specialize h₄' h_le
  refine Int.le_trans ?_ (Int.le_max_right ..)
Proof state after:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
h₄' : toFun (-f) g ≤ bound₄
⊢ ↑(|toFun f g|) ≤ max bound₃ bound₄

case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
h₄' : toFun (-f) g ≤ bound₄
⊢ ↑(|toFun f g|) ≤ max bound₃ bound₄

case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂
Tactic:
all_goals apply Int.natAbs_le' <;>
  (apply Int.le_trans (by assumption)
   solve| apply Int.le_max_left | apply Int.le_max_right)
Proof state after:
no goals
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
specialize h₁' h_ge
Proof state after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
specialize h₂' h_ge
Proof state after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
refine Int.le_trans ?_ (Int.le_max_left ..)
Proof state after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_le : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
specialize h₃' h_le
Proof state after:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
specialize h₄' h_le
Proof state after:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
h₄' : toFun (-f) g ≤ bound₄
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
h₄' : toFun (-f) g ≤ bound₄
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
refine Int.le_trans ?_ (Int.le_max_right ..)
Proof state after:
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
h₄' : toFun (-f) g ≤ bound₄
⊢ ↑(|toFun f g|) ≤ max bound₃ bound₄
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂
Tactic:
apply Int.natAbs_le' <;>
(apply Int.le_trans (by assumption)
solve| apply Int.le_max_left | apply Int.le_max_right)
Proof state after:
no goals
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ -toFun f g ≤ max bound₁ bound₂
Tactic:
apply Int.le_trans (by assumption)
Proof state after:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₂ ≤ max bound₁ bound₂
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₂ ≤ max bound₁ bound₂
Tactic:
solve| apply Int.le_max_left | apply Int.le_max_right
Proof state after:
no goals
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ -toFun f g ≤ ?m.42307
Tactic:
assumption
Proof state after:
no goals
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl.h₁
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₁ ≤ max bound₁ bound₂
Tactic:
apply Int.le_max_left
Proof state after:
no goals
Theorem: AlmostHom.bounded_of_nonneg_of_nonpos
Proof state before:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₂ ≤ max bound₁ bound₂
Tactic:
apply Int.le_max_right
Proof state after:
no goals
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof 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
Proof 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
Theorem: AlmostHom.positive_linear_growth_of_large_enough_value
Proof 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]
Proof 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