OAI/NumberTheory/EgyptianFractions/MarkedGroupingFin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.marked_grouping_units_fin line 11

   Source documentation

   Fin-indexed form of the marked grouping construction, for expansion assembly.

   theorem marked_grouping_units_fin (m q K B X : ℕ) (hm : 2 ≤ m)
       (hq : 0 < q) (hK : 0 < K) (hXq : X ≤ q)
       (hdensity : HasMarkedDivisorDensity m q)
       (hsupply : HasRationalDivisorSupply m K B) :
       ∃ k : ℕ, ∃ n : Fin k → ℕ,
         (∀ i, 0 < n i) ∧
         (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) = (X : ℚ) / ((q : ℚ) * K) ∧
         (k : ℝ) ≤ (B : ℝ) * (Real.log (X : ℝ) / (2 * Real.log (m : ℝ)) + 1) := by
   …

   Mentions: OAI.Problem337.HasMarkedDivisorDensity, OAI.Problem337.HasRationalDivisorSupply

2. theorem OAI.Problem337.GreedyDenominator.grouping_units_fin line 27

   Source documentation

   Apply marked grouping to an unreduced greedy denominator.

   theorem GreedyDenominator.grouping_units_fin {m q K B X : ℕ}
       (hq : GreedyDenominator m q) (hm : 2 ≤ m) (hK : 0 < K) (hXq : X ≤ q)
       (hsupply : HasRationalDivisorSupply m K B) :
       ∃ k : ℕ, ∃ n : Fin k → ℕ,
         (∀ i, 0 < n i) ∧
         (∑ i : Fin k, (1 : ℚ) / (n i : ℚ)) = (X : ℚ) / ((q : ℚ) * K) ∧
         (k : ℝ) ≤ (B : ℝ) * (Real.log (X : ℝ) / (2 * Real.log (m : ℝ)) + 1) :=
   …

   Mentions: OAI.Problem337.GreedyDenominator, OAI.Problem337.HasRationalDivisorSupply