OAI/NumberTheory/EgyptianFractions/DivisorSplit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.divisorSplitUpper line 10

   Source documentation

   The larger denominator in the split of 1 / n indexed by d ∣ n.

   def divisorSplitUpper (n d : ℕ) : ℕ := (n / d) * (n + d)

2. lemma OAI.Problem337.divisorSplit_quotient_ge_two line 12
3. lemma OAI.Problem337.divisorSplit_order line 21
4. lemma OAI.Problem337.divisorSplit_identity line 31
5. lemma OAI.Problem337.divisorSplitUpper_injOn line 50
6. def OAI.Problem337.countingGoodSplitDivisors line 68

   Source documentation

   A split is good when neither new denominator collides with an unchanged term.

   def countingGoodSplitDivisors (n : ℕ) (s : Finset ℕ) : Finset ℕ :=
   …

7. def OAI.Problem337.countingDivisorSplitSet line 72

   Source documentation

   Append the two denominators indexed by a divisor to a fixed unchanged set.

   def countingDivisorSplitSet (n d : ℕ) (s : Finset ℕ) : Finset ℕ :=
   …

8. lemma OAI.Problem337.countingGoodSplitDivisors_spec line 75
9. lemma OAI.Problem337.countingDivisorSplitSet_card line 82
10. lemma OAI.Problem337.countingDivisorSplitSet_sum line 89
11. lemma OAI.Problem337.countingDivisorSplitSet_injOn line 100
12. lemma OAI.Problem337.countingGoodSplitDivisors_card_bound line 123
13. lemma OAI.Problem337.countingGoodSplitDivisors_card_lower line 159
14. lemma OAI.Problem337.countingDivisorSplitSet_image_card line 170

    Source documentation

    Distinct good divisors give equally many different denominator sets.

    lemma countingDivisorSplitSet_image_card (n : ℕ) (s : Finset ℕ) :
        ((countingGoodSplitDivisors n s).image (fun d => countingDivisorSplitSet n d s)).card =
          (countingGoodSplitDivisors n s).card := by
    …

    Mentions: OAI.Problem337.countingGoodSplitDivisors, OAI.Problem337.countingDivisorSplitSet