DensityAssembly.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.densityDivisorCount line 17
Source documentation
The truncated divisor count appearing in the shifted moment hypothesis.
```
def densityDivisorCount (X : ℝ) (N : ℕ) : ℝ :=
…
```
structure OAI.Problem337.DensityBadFamily line 23
Source documentation
Explicit finite arithmetic data consumed by the density descent. No residue-distribution or divisor-moment estimate is asserted by this structure: these are the many_residues and moment_bound fields that must be supplied.
```
structure DensityBadFamily (S m ρ r c : ℝ) (d : ℕ) where
…
```
theorem OAI.Problem337.card_le_cutoff line 54

theorem OAI.Problem337.DensityBadFamily.recurrence line 62

Source documentation

Pair counting and the actual shifted divisor moment give the normalized nonlinear recurrence, including inherited bad numerators and list multiplicity.

theorem DensityBadFamily.recurrence
    {S m ρ r c : ℝ} {d : ℕ} (F : DensityBadFamily S m ρ r c d)
    (hρ0 : 0 < ρ) (hρ1 : ρ ≤ 1) (hr : 1 < r)
    (j : ℕ) (hj : j < d) :
    ((F.bad j).card : ℝ) / F.cutoff j ≤ Real.exp (-c * m) +
      Real.exp (2 * S ^ (1 / 4 : ℝ)) *
        (((F.bad (j + 1)).card : ℝ) / F.cutoff (j + 1)) ^ (1 - 1 / r) := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.DensityBadFamily

theorem OAI.Problem337.eventually_density_bad_card_le_eighth line 103

Source documentation

The full counting/analytic density conclusion, conditional on explicit residue and shifted-divisor-moment data, uniformly in all finite families.

theorem eventually_density_bad_card_le_eighth
    (c K r : ℝ) (hc : 0 < c) (hK : 0 ≤ K) (hr : 2 ≤ r) (hKr : 8 * K ≤ r) :
    ∀ᶠ S : ℝ in atTop, ∀ (m ρ : ℝ) (d : ℕ) (F : DensityBadFamily S m ρ r c d),
      S / (2 * Real.log S) ≤ m → (d : ℝ) ≤ K * Real.log S →
      0 < ρ → ρ ≤ 1 → ((F.bad 0).card : ℝ) ≤ F.cutoff 0 / 8 := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.DensityBadFamily

structure OAI.Problem337.DensityResidueFamily line 130
Source documentation
Raw residue data before the good sets are constructed. The terminal expansions, small-residue supply and shifted divisor moments are explicit inputs; all finite propagation is proved below.
```
structure DensityResidueFamily (S m ρ r c : ℝ) (d : ℕ) where
…
```
def OAI.Problem337.DensityResidueFamily.GoodSets line 170
Source documentation
The exact recursive good-set specification needed for both effects of the construction: closure counts bad residues, and decomposition propagates lists.
```
def DensityResidueFamily.GoodSets
    {S m ρ r c : ℝ} {d : ℕ} (F : DensityResidueFamily S m ρ r c d)
    (G : ℕ → Finset ℕ) : Prop :=
…
```
Mentions: OAI.Problem337.F, OAI.Problem337.DensityResidueFamily
def OAI.Problem337.DensityResidueFamily.toBadFamily line 182
Source documentation
Every small successful index for a bad numerator lands at a bad numerator at the next level. In particular a zero residue cannot remain bad.
```
def DensityResidueFamily.toBadFamily
    {S m ρ r c : ℝ} {d : ℕ} (F : DensityResidueFamily S m ρ r c d)
    (G : ℕ → Finset ℕ) (hG : F.GoodSets G) : DensityBadFamily S m ρ r c d := by
…
```
Mentions: OAI.Problem337.F, OAI.Problem337.DensityResidueFamily, OAI.Problem337.DensityBadFamily
theorem OAI.Problem337.DensityResidueFamily.good_expansions line 238
Source documentation
The same good-set specification supplies genuine unit-fraction lists; this is not an additional expansion hypothesis at intermediate levels.
```
theorem DensityResidueFamily.good_expansions
    {S m ρ r c : ℝ} {d : ℕ} (F : DensityResidueFamily S m ρ r c d)
    (G : ℕ → Finset ℕ) (hG : F.GoodSets G) :
    ∀ j ≤ d, ∀ u ∈ G j,
      Descent.UnitListAtMost ((u : ℚ) / (F.denominator * F.factor j : ℕ))
        (F.baseLength + (d - j)) := by
…
```
Mentions: OAI.Problem337.F, OAI.Problem337.DensityResidueFamily, OAI.Problem337.Descent.UnitListAtMost

theorem OAI.Problem337.eventually_residue_family_dense line 258

Source documentation

Complete finite/analytic density construction from raw residue and moment supply. The intermediate good sets and their expansions are constructed here.

theorem eventually_residue_family_dense
    (c K r : ℝ) (hc : 0 < c) (hK : 0 ≤ K) (hr : 2 ≤ r) (hKr : 8 * K ≤ r) :
    ∀ᶠ S : ℝ in atTop, ∀ (m ρ : ℝ) (d : ℕ) (F : DensityResidueFamily S m ρ r c d),
      S / (2 * Real.log S) ≤ m → (d : ℝ) ≤ K * Real.log S →
      0 < ρ → ρ ≤ 1 →
      ∃ G : Finset ℕ, G ⊆ Finset.Icc 1 ⌊F.cutoff 0⌋₊ ∧
        ((Finset.Icc 1 ⌊F.cutoff 0⌋₊ \ G).card : ℝ) ≤ F.cutoff 0 / 8 ∧
        ∀ u ∈ G, Descent.UnitListAtMost
          ((u : ℚ) / (F.denominator * F.factor 0 : ℕ)) (F.baseLength + d) := by
…

Mentions: OAI.Problem337.F, OAI.Problem337.DensityResidueFamily, OAI.Problem337.Descent.UnitListAtMost

theorem OAI.Problem337.Descent.UnitListAtMost.to_density_list_two line 278

Source documentation

Conversion to the list interface used by the elementary dense-family reduction, retaining the same length bound.

theorem Descent.UnitListAtMost.to_density_list_two {x : ℚ} {B : ℕ}
    (H : Descent.UnitListAtMost x B) (hx : x < 1) :
    ∃ l : List ℕ, (∀ n ∈ l, 2 ≤ n) ∧ l.length ≤ B ∧
      (l.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum = x := by
…

Mentions: OAI.Problem337.Descent.UnitListAtMost

theorem OAI.Problem337.eventually_residue_family_dense_lists line 292

Source documentation

A directly consumable list version of the density proposition. The only additional hypotheses are the supplied terminal-length budget and the fact that all represented fractions lie below one.

theorem eventually_residue_family_dense_lists
    (c K r : ℝ) (hc : 0 < c) (hK : 0 ≤ K) (hr : 2 ≤ r) (hKr : 8 * K ≤ r) :
    ∀ᶠ S : ℝ in atTop, ∀ (m ρ L : ℝ) (d : ℕ) (F : DensityResidueFamily S m ρ r c d),
      S / (2 * Real.log S) ≤ m → (d : ℝ) ≤ K * Real.log S →
      0 < ρ → ρ ≤ 1 →
      ((F.baseLength + d : ℕ) : ℝ) ≤ L * Real.log S →
      F.cutoff 0 < ((F.denominator * F.factor 0 : ℕ) : ℝ) →
      ∃ G : Finset ℕ,
        ((Finset.Icc 1 ⌊F.cutoff 0⌋₊ \ G).card : ℝ) ≤ F.cutoff 0 / 8 ∧
        ∀ u ∈ G, ∃ ds : List ℕ,
          (∀ n ∈ ds, 2 ≤ n) ∧ (ds.length : ℝ) ≤ L * Real.log S ∧
          (ds.map (fun n : ℕ => (1 : ℚ) / (n : ℚ))).sum =
…

Mentions: OAI.Problem337.F, OAI.Problem337.DensityResidueFamily