A natural-number block size for degree and scale

Definition

Esgk_IntrinsicPartitionScale

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsnumber-theory

This defines the natural number $(N+dj-1)/(dj)$ , with subtraction and division in the natural numbers. When $dj>0$ , it is the ceiling of $N/(dj)$ .

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Mathlib

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


namespace Esgk

 
def intrinsicPartitionBlockSize (d j N : ℕ) : ℕ :=
  (N + d * j - 1) / (d * j)


end Esgk

View graph