MarkedGrouping.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.HasMarkedDivisorDensity line 10
Source documentation
Divisors at every multiplicative scale, in the form used by grouping.
```
def HasMarkedDivisorDensity (m q : ℕ) : Prop :=
…
```

theorem OAI.Problem337.marked_grouping_step line 15

Source documentation

One group strictly shrinks the remaining numerator by a factor m².

theorem marked_grouping_step (m q X : ℕ) (hm : 2 ≤ m)
    (hX : m ^ 4 < X) (hXq : X ≤ q)
    (hdensity : HasMarkedDivisorDensity m q) :
    ∃ d s R : ℕ, 0 < d ∧ d ∣ q ∧ 1 ≤ s ∧ s ≤ m ^ 4 ∧
      X = d * s + R ∧ R * m ^ 2 < X := by
…

Mentions: OAI.Problem337.HasMarkedDivisorDensity

theorem OAI.Problem337.marked_grouping_lt_pow line 57

Source documentation

Discrete grouping bound: a numerator below (m²)^t needs at most t groups.

theorem marked_grouping_lt_pow (m q : ℕ) (hm : 2 ≤ m)
    (hdensity : HasMarkedDivisorDensity m q) (t X : ℕ)
    (hXq : X ≤ q) (hpow : X < (m ^ 2) ^ t) :
    ∃ groups : List (ℕ × ℕ), groups.length ≤ t ∧
      (∀ g ∈ groups, 0 < g.1 ∧ g.1 ∣ q ∧ 1 ≤ g.2 ∧ g.2 ≤ m ^ 4) ∧
      (groups.map (fun g => g.1 * g.2)).sum = X := by
…

Mentions: OAI.Problem337.HasMarkedDivisorDensity

theorem OAI.Problem337.marked_grouping line 96

Source documentation

The elementary grouping construction with its real logarithmic length bound.

theorem marked_grouping (m q X : ℕ) (hm : 2 ≤ m)
    (hdensity : HasMarkedDivisorDensity m q) (hXq : X ≤ q) :
    ∃ groups : List (ℕ × ℕ),
      (groups.length : ℝ) ≤ Real.log (X : ℝ) / (2 * Real.log (m : ℝ)) + 1 ∧
      (∀ g ∈ groups, 0 < g.1 ∧ g.1 ∣ q ∧ 1 ≤ g.2 ∧ g.2 ≤ m ^ 4) ∧
      (groups.map (fun g => g.1 * g.2)).sum = X := by
…

Mentions: OAI.Problem337.HasMarkedDivisorDensity