MarkedGroupingUnits.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.rational_divisor_unit line 10

Source documentation

A rational with numerator dividing K, after scaling, is a unit fraction.

theorem rational_divisor_unit (q K d e t : ℕ) (hq : 0 < q) (hK : 0 < K)
    (hd : 0 < d) (hdq : d ∣ q) (he : 0 < e) (heK : e ∣ K) (ht : 0 < t) :
    0 < (q / d) * (K / e) * t ∧
    (1 : ℚ) / (((q / d) * (K / e) * t : ℕ) : ℚ) =
      ((d : ℚ) / ((q : ℚ) * (K : ℚ))) * ((e : ℚ) / (t : ℚ)) := by
…

def OAI.Problem337.HasRationalDivisorSupply line 30
Source documentation
A supply expresses every small integer as a short sum of rational divisors.
```
def HasRationalDivisorSupply (m K B : ℕ) : Prop :=
…
```

theorem OAI.Problem337.supplied_group_units line 37

Source documentation

Convert a single supplied group to positive unit fractions.

theorem supplied_group_units (m q K B d s : ℕ) (hq : 0 < q) (hK : 0 < K)
    (hd : 0 < d) (hdq : d ∣ q) (hs : 1 ≤ s) (hsm : s ≤ m ^ 4)
    (hsupply : HasRationalDivisorSupply m K B) :
    ∃ denoms : List ℕ, denoms.length ≤ B ∧ (∀ n ∈ denoms, 0 < n) ∧
      (denoms.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum =
        ((d : ℚ) * (s : ℚ)) / ((q : ℚ) * (K : ℚ)) := by
…

Mentions: OAI.Problem337.HasRationalDivisorSupply

theorem OAI.Problem337.supplied_groups_units line 62

Source documentation

Concatenate supplied groups, retaining a linear length budget.

theorem supplied_groups_units (m q K B : ℕ) (hq : 0 < q) (hK : 0 < K)
    (hsupply : HasRationalDivisorSupply m K B) (groups : List (ℕ × ℕ))
    (hgroups : ∀ g ∈ groups, 0 < g.1 ∧ g.1 ∣ q ∧ 1 ≤ g.2 ∧ g.2 ≤ m ^ 4) :
    ∃ denoms : List ℕ, denoms.length ≤ B * groups.length ∧
      (∀ n ∈ denoms, 0 < n) ∧
      (denoms.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum =
        (((groups.map (fun g => g.1 * g.2)).sum : ℕ) : ℚ) / ((q : ℚ) * (K : ℚ)) := by
…

Mentions: OAI.Problem337.HasRationalDivisorSupply

theorem OAI.Problem337.marked_grouping_units_from_list_supply line 91

Source documentation

Grouping a numerator using a rational-divisor supply yields a short unit-fraction list. No distinctness is asserted here; later cleanup is applied only to the tail.

theorem marked_grouping_units_from_list_supply (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) :
    ∃ denoms : List ℕ,
      (denoms.length : ℝ) ≤ (B : ℝ) *
        (Real.log (X : ℝ) / (2 * Real.log (m : ℝ)) + 1) ∧
      (∀ n ∈ denoms, 0 < n) ∧
      (denoms.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum =
        (X : ℚ) / ((q : ℚ) * (K : ℚ)) := by
…

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