FiniteBox.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.finite_ncard_le_box line 9

Source documentation

Counting positive integer functions in a varying finite box.

theorem finite_ncard_le_box {ι : Type*} [Fintype ι]
    (S : Set (ι → ℕ)) (B : ι → ℕ)
    (hS : ∀ n ∈ S, ∀ i, 1 ≤ n i ∧ n i ≤ B i) :
    S.Finite ∧ S.ncard ≤ ∏ i, B i := by
…

theorem OAI.Problem337.sum_two_pow_fin line 29
Source documentation
Geometric exponent sum for the denominator box.
```
theorem sum_two_pow_fin (k : ℕ) :
    (∑ i : Fin k, 2 ^ i.val) = 2 ^ k - 1 := by
…
```
theorem OAI.Problem337.prod_egyptian_bounds line 41
Source documentation
The denominator box appearing in the counting bound has the stated size.
```
theorem prod_egyptian_bounds (k : ℕ) :
    (∏ i : Fin k, k ^ (2 ^ i.val)) = k ^ (2 ^ k - 1) := by
…
```

theorem OAI.Problem337.finite_ncard_le_egyptian_box line 46

Source documentation

Pointwise denominator bounds give finiteness and the sharp box-count estimate.

theorem finite_ncard_le_egyptian_box (k : ℕ) (S : Set (Fin k → ℕ))
    (hpos : ∀ n ∈ S, ∀ i, 1 ≤ n i)
    (hbound : ∀ n ∈ S, ∀ i, n i ≤ k ^ (2 ^ i.val)) :
    S.Finite ∧ S.ncard ≤ k ^ (2 ^ k - 1) := by
…