RawDensityUpper.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RawDensitySupply line 13
Source documentation
The remaining arithmetic supply interface for the main upper bound. The residue distribution and shifted divisor moments are explicit fields of DensityResidueFamily; this definition does not assert their existence.
```
def RawDensitySupply (DM L c K r S : ℝ) (C : ℕ) : Prop :=
…
```

theorem OAI.Problem337.eventually_dense_family_of_raw_supply line 24

Source documentation

The checked density descent supplies exactly the input to the elementary main-upper reduction. No additional fraction-size hypothesis is needed.

theorem eventually_dense_family_of_raw_supply
    (DM L c K r : ℝ) (hDM : 1 < DM) (hc : 0 < c) (hK : 0 ≤ K)
    (hr : 2 ≤ r) (hKr : 8 * K ≤ r) :
    ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      RawDensitySupply DM L c K r S C → DenseEgyptianFamily DM L S C := by
…

Mentions: OAI.Problem337.RawDensitySupply, OAI.Problem337.DenseEgyptianFamily

theorem OAI.Problem337.main_upper_of_raw_density_supply line 52

Source documentation

Final composition of the two checked reductions. The sole remaining construction premise is eventual existence of the raw arithmetic supply.

theorem main_upper_of_raw_density_supply
    (DM L c K r : ℝ) (hDM : 1 < DM) (hL : 0 < L)
    (hc : 0 < c) (hK : 0 ≤ K) (hr : 2 ≤ r) (hKr : 8 * K ≤ r)
    (hsupply : ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * S) →
      RawDensitySupply DM L c K r S C) :
    ∃ c2 : ℝ, 0 < c2 ∧ ∃ b0 : ℕ, ∀ b : ℕ, b0 ≤ b →
      (maxEgyptianLength b : ℝ) ≤ c2 * Real.log (Real.log (b : ℝ)) := by
…

Mentions: OAI.Problem337.RawDensitySupply, OAI.Problem337.maxEgyptianLength