GeometricSupplyAsymptotic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.GeometricDensity.HasSupply line 13
Source documentation
The remaining arithmetic existence interface at a fixed scale. It includes the actual common denominator, normalized residue lists, and terminal residue supply. The localization loss may vary with the scale.
```
def HasSupply (DM D₀ η c r A B S : ℝ) (C : ℕ) : Prop :=
…
```

theorem OAI.Problem337.GeometricDensity.eventually_raw_density_supply_of_geometric line 23

Source documentation

All scale, floor, geometric-depth, and localization-loss thresholds are uniform in the original integer factor. Thus actual geometric supply is the only arithmetic premise left in the raw density family interface.

theorem eventually_raw_density_supply_of_geometric
    (DM D₀ η c r A B : ℝ)
    (hDM : 1 < DM) (hD₀ : 1 ≤ D₀) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hr : 1 ≤ r) :
    ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      HasSupply DM D₀ η c r A B S C →
      RawDensitySupply DM
        (TerminalAssembly.terminalCoefficient D₀ (1 - η) + 3 * (DM + 2) / η + 1)
        c (3 * (DM + 2) / η) r S C := by
…

Mentions: OAI.Problem337.GeometricDensity.HasSupply, OAI.Problem337.RawDensitySupply, OAI.Problem337.TerminalAssembly.terminalCoefficient

theorem OAI.Problem337.GeometricDensity.main_upper_of_geometric_supply line 48

Source documentation

The complete main-upper pipeline, with precisely the actual arithmetic supply left as an explicit eventual hypothesis. No extra density or expansion hypotheses are needed after the geometric data have been constructed.

theorem main_upper_of_geometric_supply
    (DM D₀ η c r A B : ℝ)
    (hDM : 1 < DM) (hD₀ : 1 ≤ D₀) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
    (hc : 0 < c) (hA : 0 ≤ A) (hB : 0 ≤ B) (hr : 2 ≤ r)
    (hKr : 8 * (3 * (DM + 2) / η) ≤ r)
    (hsupply : ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * S) →
      HasSupply DM D₀ η c r A B S C) :
    ∃ c2 : ℝ, 0 < c2 ∧ ∃ b0 : ℕ, ∀ b : ℕ, b0 ≤ b →
      (maxEgyptianLength b : ℝ) ≤ c2 * Real.log (Real.log (b : ℝ)) := by
…

Mentions: OAI.Problem337.GeometricDensity.HasSupply, OAI.Problem337.maxEgyptianLength