DivisorBranching.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.divisorSplitSmall line 9
Source documentation
The two replacement denominators associated to a proper divisor.
```
def divisorSplitSmall (n d : ℕ) : ℕ := n + d
```
def OAI.Problem337.divisorSplitLarge line 10
lemma OAI.Problem337.divisor_split_data line 12
lemma OAI.Problem337.divisor_split_identity line 24
lemma OAI.Problem337.divisor_split_small_injective line 36
lemma OAI.Problem337.divisor_split_large_injOn line 41

lemma OAI.Problem337.filter_avoiding_two_card line 57

Source documentation

Two injective collision maps remove at most twice the size of the forbidden set.

lemma filter_avoiding_two_card {α β : Type*} [DecidableEq α] [DecidableEq β]
    (I : Finset α) (T : Finset β) (f g : α → β)
    (hf : Set.InjOn f (↑I : Set α)) (hg : Set.InjOn g (↑I : Set α)) :
    I.card ≤ (I.filter (fun d => f d ∉ T ∧ g d ∉ T)).card + 2*T.card := by
…

def OAI.Problem337.goodSplitDivisors line 88
Source documentation
Proper divisors whose two new denominators avoid all fixed denominators.
```
def goodSplitDivisors (n : ℕ) (T : Finset ℕ) : Finset ℕ :=
…
```
lemma OAI.Problem337.good_split_divisors_card line 91
def OAI.Problem337.divisorSplitSet line 104
Source documentation
Replace one denominator, keeping the other denominators in T.
```
def divisorSplitSet (n : ℕ) (T : Finset ℕ) (d : ℕ) : Finset ℕ :=
…
```
lemma OAI.Problem337.good_split_divisor_data line 107
lemma OAI.Problem337.divisor_split_set_card line 115
lemma OAI.Problem337.divisor_split_set_sum line 123
lemma OAI.Problem337.divisor_split_set_positive line 135
lemma OAI.Problem337.divisor_split_set_injOn line 147

theorem OAI.Problem337.divisor_branching_family line 165

Source documentation

An expansion containing a highly divisible denominator branches into many distinct expansions, all with precisely one additional term.

theorem divisor_branching_family (S : Finset ℕ)
    (hpos : ∀ x ∈ S, 0 < x) (hsum : (∑ x ∈ S, (1 : ℚ) / x) = 1)
    (n : ℕ) (hn : n ∈ S) :
    ∃ U : Finset (Finset ℕ),
      n.divisors.card ≤ U.card + 2*(S.card - 1) + 1 ∧
      ∀ T ∈ U, T.card = S.card + 1 ∧
        (∀ x ∈ T, 0 < x) ∧ (∑ x ∈ T, (1 : ℚ) / x) = 1 := by
…