MainUpperReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.DenseEgyptianFamily line 15
Source documentation
The exact dense-family input required by the elementary main upper reduction. No distinctness is asked of the supplied lists.
```
def DenseEgyptianFamily (DM L S : ℝ) (C : ℕ) : Prop :=
…
```

theorem OAI.Problem337.egyptianLength_le_list_length line 26

Source documentation

A positive unit-fraction list below one controls the actual minimum length.

theorem egyptianLength_le_list_length {a b : ℕ} (hab : a < b)
    (l : List ℕ) (hden : ∀ d ∈ l, 2 ≤ d)
    (hsum : (l.map (fun d : ℕ => (1 : ℚ) / (d : ℚ))).sum =
      (a : ℚ) / (b : ℚ)) : egyptianLength a b ≤ l.length := by
…

Mentions: OAI.Problem337.egyptianLength

theorem OAI.Problem337.egyptianLength_upper_of_dense_at line 38

Source documentation

For one fixed large denominator, the dense input and greedy preparation give an explicit uniform length coefficient.

theorem egyptianLength_upper_of_dense_at
    (DM L : ℝ) (hDM : 1 < DM) (hL : 0 < L)
    (b N : ℕ) (hb : 2 ≤ b) (hS : Real.exp 1 ≤ Real.log (b : ℝ))
    (hbudget : ((N + 1 : ℕ) : ℝ) ≤
      (2 / Real.log 2 + 2) * Real.log (Real.log (b : ℝ)))
    (hcap : Real.exp (4 * (DM + 2) * Real.log (b : ℝ)) *
      (1 / 2 : ℝ) ^ (2 ^ N) ≤ 1)
    (hdensity : ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * Real.log (b : ℝ)) ≤ (C : ℝ) →
      (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * Real.log (b : ℝ)) →
      DenseEgyptianFamily DM L (Real.log (b : ℝ)) C) :
    ∀ a : ℕ, 1 ≤ a → a < b →
…

Mentions: OAI.Problem337.DenseEgyptianFamily

theorem OAI.Problem337.main_upper_of_dense_family line 120

Source documentation

Complete elementary reduction of the uniform upper bound to the dense-family proposition. All other inputs (greedy stopping, splitting, and distinctification) are proved in the imported modules.

theorem main_upper_of_dense_family
    (DM L S0 : ℝ) (hDM : 1 < DM) (hL : 0 < L)
    (hdensity : ∀ S : ℝ, S0 ≤ S → ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * S) →
      DenseEgyptianFamily DM L S C) :
    ∃ c2 : ℝ, 0 < c2 ∧ ∃ b0 : ℕ, ∀ b : ℕ, b0 ≤ b →
      (maxEgyptianLength b : ℝ) ≤ c2 * Real.log (Real.log (b : ℝ)) := by
…

Mentions: OAI.Problem337.DenseEgyptianFamily, OAI.Problem337.maxEgyptianLength