Mathlib.Data.Int.LeastGreatest

Module docstring

{"# Least upper bound and greatest lower bound properties for integers

In this file we prove that a bounded above nonempty set of integers has the greatest element, and a counterpart of this statement for the least element.

Main definitions

Int.leastOfBdd: if P : ℤ → Prop is a decidable predicate, b is a lower bound of the set {m | P m}, and there exists m : ℤ such that P m (this time, no witness is required), then Int.leastOfBdd returns the least number m such that P m, together with proofs of P m and of the minimality. This definition is computable and does not rely on the axiom of choice.
Int.greatestOfBdd: a similar definition with all inequalities reversed.

Main statements

Int.exists_least_of_bdd: if P : ℤ → Prop is a predicate such that the set {m : P m} is bounded below and nonempty, then this set has the least element. This lemma uses classical logic to avoid assumption [DecidablePred P]. See Int.leastOfBdd for a constructive counterpart.
Int.coe_leastOfBdd_eq: (Int.leastOfBdd b Hb Hinh : ℤ) does not depend on b.
Int.exists_greatest_of_bdd, Int.coe_greatest_of_bdd_eq: versions of the above lemmas with all inequalities reversed.

Tags

integer numbers, least element, greatest element "}

Int.leastOfBdd definition

 {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z) (Hinh : ∃ z : ℤ, P z) :
  { lb : ℤ // P lb ∧ ∀ z : ℤ, P z → lb ≤ z }

Full source

/-- A computable version of `exists_least_of_bdd`: given a decidable predicate on the
integers, with an explicit lower bound and a proof that it is somewhere true, return
the least value for which the predicate is true. -/
def leastOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z)
    (Hinh : ∃ z : ℤ, P z) : { lb : ℤ // P lb ∧ ∀ z : ℤ, P z → lb ≤ z } :=
  have EX : ∃ n : ℕ, P (b + n) :=
    let ⟨elt, Helt⟩ := Hinh
    match elt, le.dest (Hb _ Helt), Helt with
    | _, ⟨n, rfl⟩, Hn => ⟨n, Hn⟩
  ⟨b + (Nat.find EX : ℤ), Nat.find_spec EX, fun z h =>
    match z, le.dest (Hb _ h), h with
    | _, ⟨_, rfl⟩, h => add_le_add_left (Int.ofNat_le.2 <| Nat.find_min' _ h) _⟩

Least integer satisfying a predicate with lower bound

Informal description

Given a decidable predicate $ P $ on the integers, an explicit lower bound $ b $ for the set $\{ z \mid P z \}$, and a proof that there exists some integer satisfying $ P $, the function `Int.leastOfBdd` returns the least integer $ \text{lb} $ such that $ P(\text{lb}) $ holds, along with proofs that $ P(\text{lb}) $ is true and that $ \text{lb} $ is minimal (i.e., for any integer $ z $ satisfying $ P(z) $, $ \text{lb} \leq z $).

Int.isLeast_coe_leastOfBdd theorem

 {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z) (Hinh : ∃ z : ℤ, P z) :
  IsLeast {z | P z} (leastOfBdd b Hb Hinh : ℤ)

Full source

/-- `Int.leastOfBdd` is the least integer satisfying a predicate which is false for all `z : ℤ` with
`z < b` for some fixed `b : ℤ`. -/
lemma isLeast_coe_leastOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z)
    (Hinh : ∃ z : ℤ, P z) : IsLeast {z | P z} (leastOfBdd b Hb Hinh : ℤ) :=
  (leastOfBdd b Hb Hinh).2

Least Integer Satisfying Predicate is Minimal in Bounded Below Set

Informal description

For any decidable predicate $P$ on the integers $\mathbb{Z}$, given a lower bound $b$ such that $b \leq z$ for all $z$ satisfying $P(z)$, and a proof that there exists some integer satisfying $P$, the integer $\text{lb}$ returned by $\text{Int.leastOfBdd}$ is the least element of the set $\{z \mid P(z)\}$. That is, $\text{lb}$ satisfies $P(\text{lb})$ and is minimal in the sense that for any $z$ satisfying $P(z)$, we have $\text{lb} \leq z$.

Int.exists_least_of_bdd theorem

 {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, P z → b ≤ z) (Hinh : ∃ z : ℤ, P z) : ∃ lb : ℤ, P lb ∧ ∀ z : ℤ, P z → lb ≤ z

Full source

/--
If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded below and nonempty,
then this set has the least element. This lemma uses classical logic to avoid assumption
`[DecidablePred P]`. See `Int.leastOfBdd` for a constructive counterpart. -/
theorem exists_least_of_bdd
    {P : ℤ → Prop}
    (Hbdd : ∃ b : ℤ, ∀ z : ℤ, P z → b ≤ z)
    (Hinh : ∃ z : ℤ, P z) : ∃ lb : ℤ, P lb ∧ ∀ z : ℤ, P z → lb ≤ z := by
  classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
  exact ⟨lb, H⟩

Existence of Least Element in Bounded Below Nonempty Integer Sets

Informal description

For any predicate $ P $ on the integers, if the set $\{ z \in \mathbb{Z} \mid P(z) \}$ is nonempty and bounded below (i.e., there exists $ b \in \mathbb{Z} $ such that $ b \leq z $ for all $ z $ satisfying $ P(z) $), then there exists a least integer $ \text{lb} $ such that $ P(\text{lb}) $ holds and $ \text{lb} \leq z $ for all $ z $ satisfying $ P(z) $.

Int.coe_leastOfBdd_eq theorem

 {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → b ≤ z) (Hb' : ∀ z : ℤ, P z → b' ≤ z)
  (Hinh : ∃ z : ℤ, P z) : (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh

Full source

theorem coe_leastOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → b ≤ z)
    (Hb' : ∀ z : ℤ, P z → b' ≤ z) (Hinh : ∃ z : ℤ, P z) :
    (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh := by
  rcases leastOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
  rcases leastOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
  exact le_antisymm (h2n _ hn') (h2n' _ hn)

Independence of Least Integer from Lower Bound Choice

Informal description

For any decidable predicate $P$ on the integers $\mathbb{Z}$, and for any two lower bounds $b$ and $b'$ of the set $\{z \mid P(z)\}$, the least integer satisfying $P$ computed with respect to $b$ is equal to the least integer satisfying $P$ computed with respect to $b'$. In other words, the value of $\text{leastOfBdd}$ does not depend on the choice of lower bound.

Int.greatestOfBdd definition

 {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → z ≤ b) (Hinh : ∃ z : ℤ, P z) :
  { ub : ℤ // P ub ∧ ∀ z : ℤ, P z → z ≤ ub }

Full source

/-- A computable version of `exists_greatest_of_bdd`: given a decidable predicate on the
integers, with an explicit upper bound and a proof that it is somewhere true, return
the greatest value for which the predicate is true. -/
def greatestOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → z ≤ b)
    (Hinh : ∃ z : ℤ, P z) : { ub : ℤ // P ub ∧ ∀ z : ℤ, P z → z ≤ ub } :=
  have Hbdd' : ∀ z : ℤ, P (-z) → -b ≤ z := fun _ h => neg_le.1 (Hb _ h)
  have Hinh' : ∃ z : ℤ, P (-z) :=
    let ⟨elt, Helt⟩ := Hinh
    ⟨-elt, by rw [neg_neg]; exact Helt⟩
  let ⟨lb, Plb, al⟩ := leastOfBdd (-b) Hbdd' Hinh'
  ⟨-lb, Plb, fun z h => le_neg.1 <| al _ <| by rwa [neg_neg]⟩

Greatest integer satisfying a predicate with upper bound

Informal description

Given a decidable predicate $ P $ on the integers, an explicit upper bound $ b $ for the set $\{ z \mid P z \}$, and a proof that there exists some integer satisfying $ P $, the function `Int.greatestOfBdd` returns the greatest integer $ \text{ub} $ such that $ P(\text{ub}) $ holds, along with proofs that $ P(\text{ub}) $ is true and that $ \text{ub} $ is maximal (i.e., for any integer $ z $ satisfying $ P(z) $, $ z \leq \text{ub} $).

Int.isGreatest_coe_greatestOfBdd theorem

 {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → z ≤ b) (Hinh : ∃ z : ℤ, P z) :
  IsGreatest {z | P z} (greatestOfBdd b Hb Hinh : ℤ)

Full source

/-- `Int.greatestOfBdd` is the greatest integer satisfying a predicate which is false for all
`z : ℤ` with `b < z` for some fixed `b : ℤ`. -/
lemma isGreatest_coe_greatestOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ)
    (Hb : ∀ z : ℤ, P z → z ≤ b) (Hinh : ∃ z : ℤ, P z) :
    IsGreatest {z | P z} (greatestOfBdd b Hb Hinh : ℤ) :=
  (greatestOfBdd b Hb Hinh).2

Greatest Integer Satisfying a Predicate is the Greatest Element of the Set

Informal description

Let $ P $ be a decidable predicate on the integers $\mathbb{Z}$, $ b $ an integer such that $ P(z) $ implies $ z \leq b $ for all $ z $, and suppose there exists some integer satisfying $ P $. Then the integer $\text{greatestOfBdd}\ b\ Hb\ Hinh$ is the greatest element of the set $\{ z \mid P(z) \}$, meaning it satisfies $ P $ and is an upper bound for all integers satisfying $ P $.

Int.exists_greatest_of_bdd theorem

 {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, P z → z ≤ b) (Hinh : ∃ z : ℤ, P z) : ∃ ub : ℤ, P ub ∧ ∀ z : ℤ, P z → z ≤ ub

Full source

/--
If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded above and nonempty,
then this set has the greatest element. This lemma uses classical logic to avoid assumption
`[DecidablePred P]`. See `Int.greatestOfBdd` for a constructive counterpart. -/
theorem exists_greatest_of_bdd
    {P : ℤ → Prop}
    (Hbdd : ∃ b : ℤ, ∀ z : ℤ, P z → z ≤ b)
    (Hinh : ∃ z : ℤ, P z) : ∃ ub : ℤ, P ub ∧ ∀ z : ℤ, P z → z ≤ ub := by
  classical
  let ⟨b, Hb⟩ := Hbdd
  let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
  exact ⟨lb, H⟩

Existence of Greatest Integer in a Bounded Nonempty Set

Informal description

Let $P : \mathbb{Z} \to \text{Prop}$ be a predicate on the integers. If the set $\{z \mid P(z)\}$ is nonempty and bounded above (i.e., there exists an integer $b$ such that $P(z)$ implies $z \leq b$ for all $z$), then there exists a greatest integer $\text{ub}$ satisfying $P(\text{ub})$, and for any integer $z$ satisfying $P(z)$, we have $z \leq \text{ub}$.

Int.coe_greatestOfBdd_eq theorem

 {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → z ≤ b) (Hb' : ∀ z : ℤ, P z → z ≤ b')
  (Hinh : ∃ z : ℤ, P z) : (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh

Full source

theorem coe_greatestOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ}
    (Hb : ∀ z : ℤ, P z → z ≤ b) (Hb' : ∀ z : ℤ, P z → z ≤ b') (Hinh : ∃ z : ℤ, P z) :
    (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh := by
  rcases greatestOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
  rcases greatestOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
  exact le_antisymm (h2n' _ hn) (h2n _ hn')

Independence of Greatest Integer from Upper Bound Choice

Informal description

Let $P : \mathbb{Z} \to \text{Prop}$ be a decidable predicate on the integers. Suppose there exist integers $b$ and $b'$ such that for any integer $z$, if $P(z)$ holds then $z \leq b$ and $z \leq b'$. If there exists some integer satisfying $P$, then the greatest integer satisfying $P$ (computed with respect to $b$) is equal to the greatest integer satisfying $P$ (computed with respect to $b'$). In other words, the value of $\text{greatestOfBdd}$ does not depend on the choice of upper bound $b$ or $b'$.