ResidueStep.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.nat_ceiling_residue line 9
Source documentation
The natural-number ceiling algorithm, including its least nonnegative residue.
```
theorem nat_ceiling_residue (N u : ℕ) (hN : 0 < N) (hu : 0 < u) :
    ∃ z h : ℕ, 0 < z ∧ h < u ∧ N + h = u * z := by
…
```

theorem OAI.Problem337.residue_step_identity line 23

Source documentation

The division step underlying both the terminal and backward numerator descent.

theorem residue_step_identity (M Q u t z h : ℕ)
    (hM : 0 < M) (hQ : 0 < Q) (ht : 0 < t) (hz : 0 < z)
    (htM : t ∣ M) (hres : Q * t + h = u * z) :
    (u : ℚ) / (M * Q : ℕ) =
      (1 : ℚ) / ((M / t) * z : ℕ) +
        (1 : ℚ) / z * ((h : ℚ) / (M * Q : ℕ)) := by
…

theorem OAI.Problem337.unit_fraction_list_scale line 43

Source documentation

Rescale an arbitrary positive unit-fraction list by a positive integer.

theorem unit_fraction_list_scale {k : ℕ} (n : Fin k → ℕ) (z : ℕ)
    (hn : ∀ i, 0 < n i) (hz : 0 < z) :
    (∀ i, 0 < z * n i) ∧
      (∑ i : Fin k, (1 : ℚ) / (z * n i : ℕ)) =
        (1 : ℚ) / z * (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) := by
…

theorem OAI.Problem337.residue_step_list line 57

Source documentation

Adjoining the unit fraction produced by a residue step lifts any expansion of the smaller numerator. Repeated denominators are deliberately permitted.

theorem residue_step_list {k : ℕ} (M Q u t z h : ℕ)
    (hM : 0 < M) (hQ : 0 < Q) (ht : 0 < t) (hz : 0 < z)
    (htM : t ∣ M) (hres : Q * t + h = u * z)
    (n : Fin k → ℕ) (hn : ∀ i, 0 < n i)
    (hsum : (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) = (h : ℚ) / (M * Q : ℕ)) :
    ∃ n' : Fin (k + 1) → ℕ, (∀ i, 0 < n' i) ∧
      (∑ i : Fin (k + 1), (1 : ℚ) / (n' i : ℚ)) = (u : ℚ) / (M * Q : ℕ) := by
…

theorem OAI.Problem337.unit_fraction_list_change_factor line 77

Source documentation

Passing from a smaller denominator factor to a divisible larger one only scales all unit denominators, and does not add terms.

theorem unit_fraction_list_change_factor {k : ℕ} (M Q Qnext h : ℕ)
    (hM : 0 < M) (hQ : 0 < Q) (hQnext : 0 < Qnext) (hdiv : Qnext ∣ Q)
    (n : Fin k → ℕ) (hn : ∀ i, 0 < n i)
    (hsum : (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) =
      (h : ℚ) / (M * Qnext : ℕ)) :
    ∃ n' : Fin k → ℕ, (∀ i, 0 < n' i) ∧
      (∑ i : Fin k, (1 : ℚ) / (n' i : ℚ)) = (h : ℚ) / (M * Q : ℕ) := by
…

theorem OAI.Problem337.residue_step_list_change_factor line 100

Source documentation

The full backward step, allowing the denominator factor to change by an integer divisor between adjacent levels.

theorem residue_step_list_change_factor {k : ℕ} (M Q Qnext u t z h : ℕ)
    (hM : 0 < M) (hQ : 0 < Q) (hQnext : 0 < Qnext)
    (ht : 0 < t) (hz : 0 < z) (htM : t ∣ M) (hdiv : Qnext ∣ Q)
    (hres : Q * t + h = u * z)
    (n : Fin k → ℕ) (hn : ∀ i, 0 < n i)
    (hsum : (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) =
      (h : ℚ) / (M * Qnext : ℕ)) :
    ∃ n' : Fin (k + 1) → ℕ, (∀ i, 0 < n' i) ∧
      (∑ i : Fin (k + 1), (1 : ℚ) / (n' i : ℚ)) = (u : ℚ) / (M * Q : ℕ) := by
…

theorem OAI.Problem337.unit_fraction_denominators_two_of_sum_lt_one line 115

Source documentation

Every positive unit fraction in a list of total less than one has an integer denominator at least two.

theorem unit_fraction_denominators_two_of_sum_lt_one {k : ℕ} (n : Fin k → ℕ)
    (hn : ∀ i, 0 < n i)
    (hsum : (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) < 1) :
    ∀ i, 2 ≤ n i := by
…