OAI/NumberTheory/EgyptianFractions/DivisorDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.DivisorDense line 9

   Source documentation

   A positive integer has a divisor within a factor of m below each scale.

   def DivisorDense (m q : ℕ) : Prop :=
   …

2. theorem OAI.Problem337.divisorDense_base line 13
3. theorem OAI.Problem337.DivisorDense.mul line 20
4. inductive OAI.Problem337.GreedyDenominator line 54

   Source documentation

   Denominators produced by multiplying by positive integers at most one more than the preceding denominator, without reducing fractions.

   inductive GreedyDenominator (m : ℕ) : ℕ → Prop
     | base : GreedyDenominator m m
     | mul {q n : ℕ} : GreedyDenominator m q → 1 ≤ n → n ≤ q + 1 →
         GreedyDenominator m (n * q)

5. theorem OAI.Problem337.GreedyDenominator.positive line 59
6. theorem OAI.Problem337.GreedyDenominator.divisorDense line 65
7. theorem OAI.Problem337.marked_divisor_density line 72