RemoveRepetitions.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.reciprocal_pair_replacement line 9

Source documentation

Replacing two equal unit fractions by two unequal smaller-first terms.

theorem reciprocal_pair_replacement (m : ℕ) (hm : 3 ≤ m) :
    ∃ a b : ℕ, 1 ≤ a ∧ 1 ≤ b ∧ a < m ∧
      (1 : ℚ) / a + 1 / b = 1 / m + 1 / m := by
…

theorem OAI.Problem337.reciprocal_sum_update line 27

Source documentation

Effect of a one-coordinate replacement on a finite reciprocal sum.

theorem reciprocal_sum_update {k : ℕ} (n : Fin k → ℕ) (i : Fin k) (a : ℕ) :
    (∑ t, (1 : ℚ) / (Function.update n i a t : ℚ)) =
      (∑ t, (1 : ℚ) / (n t : ℚ)) + 1 / (a : ℚ) - 1 / (n i : ℚ) := by
…

theorem OAI.Problem337.reciprocal_sum_update_two line 37

Source documentation

Two-coordinate replacement preserves the sum when the two reciprocals agree.

theorem reciprocal_sum_update_two {k : ℕ} (n : Fin k → ℕ) {i j : Fin k}
    (hij : i ≠ j) (a b : ℕ)
    (hab : (1 : ℚ) / a + 1 / b = 1 / n i + 1 / n j) :
    (∑ t, (1 : ℚ) / (Function.update (Function.update n i a) j b t : ℚ)) =
      ∑ t, (1 : ℚ) / (n t : ℚ) := by
…

theorem OAI.Problem337.lex_update_two_lt line 47

Source documentation

Any first-coordinate decrease beats a later-coordinate change lexicographically.

theorem lex_update_two_lt {k : ℕ} (n : Fin k → ℕ) {i j : Fin k}
    (hij : i < j) (a b : ℕ) (ha : a < n i) :
    Pi.Lex (· < ·) (· < ·) (Function.update (Function.update n i a) j b) n := by
…

theorem OAI.Problem337.exists_strictMono_of_two_replacements line 56

Source documentation

A reusable lexicographic minimization principle for constrained tuples.

theorem exists_strictMono_of_two_replacements {k : ℕ}
    (P : (Fin k → ℕ) → Prop) (hP : ∃ n, P n)
    (hstep : ∀ n, P n → ∀ i j : Fin k, i < j → n j ≤ n i →
      ∃ a b : ℕ, a < n i ∧ P (Function.update (Function.update n i a) j b)) :
    ∃ n, P n ∧ StrictMono n := by
…

theorem OAI.Problem337.remove_repetitions_below_one line 72

Source documentation

Takenouchi cleanup, proved using a lexicographically least tuple. No distinctness or ordering is required of the original representation.

theorem remove_repetitions_below_one {k : ℕ} (x : ℚ)
    (hx : x < 1) (original : Fin k → ℕ)
    (hpos : ∀ i, 1 ≤ original i)
    (hsum : (∑ i, (1 : ℚ) / (original i : ℚ)) = x) :
    ∃ n : Fin k → ℕ, (∀ i, 2 ≤ n i) ∧ StrictMono n ∧
      (∑ i, (1 : ℚ) / (n i : ℚ)) = x := by
…