OAI/NumberTheory/EgyptianFractions/DivisorCounting.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.finset_family_card_le_F line 12

   Source documentation

   A finite family of distinct denominator sets produces the same number of increasing one-expansions.

   lemma finset_family_card_le_F (family : Finset (Finset ℕ)) (k : ℕ)
       (hfinite : (OneExpansions k).Finite)
       (hfamily : ∀ s ∈ family, s.card = k ∧
         (∀ m ∈ s, 1 ≤ m) ∧ (∑ m ∈ s, (1 : ℚ) / m) = 1) :
       family.card ≤ F k := by
   …

   Mentions: OAI.Problem337.OneExpansions, OAI.Problem337.F

2. lemma OAI.Problem337.countingDivisorSplitSet_positive line 41
3. theorem OAI.Problem337.divisor_branching_lower_bound line 54

   Source documentation

   Branching over all noncolliding proper divisors of one denominator.

   theorem divisor_branching_lower_bound (s : Finset ℕ) (n : ℕ)
       (hn : n ∈ s) (hpos : ∀ m ∈ s, 1 ≤ m)
       (hsum : (∑ m ∈ s, (1 : ℚ) / m) = 1)
       (hfinite : (OneExpansions (s.card + 1)).Finite) :
       n.divisors.card - 1 - 2 * (s.card - 1) ≤ F (s.card + 1) := by
   …

   Mentions: OAI.Problem337.OneExpansions, OAI.Problem337.F