GeometricRawDensity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.positive_ceiling_quotient line 15
Source documentation
A positive integer shift has a positive natural ceiling quotient.
```
lemma positive_ceiling_quotient {N u : ℕ} (hN : 0 < N) (hu : 0 < u) :
    0 < ⌈(N : ℝ) / u⌉₊ := by
…
```

lemma OAI.Problem337.ceiling_residue_le_of_fract_lt line 23

Source documentation

A normalized small negative residue gives the unnormalized ceiling bound used by the backward construction. The cutoff need not be integral.

lemma ceiling_residue_le_of_fract_lt {N u : ℕ} {ρ X : ℝ}
    (hu : 0 < u) (hρ : 0 ≤ ρ) (huX : (u : ℝ) ≤ X)
    (hsmall : Int.fract (-(N : ℝ) / u) < ρ) :
    ((u * ⌈(N : ℝ) / u⌉₊ - N : ℕ) : ℝ) ≤ ρ * X := by
…

lemma OAI.Problem337.terminal_step_of_fract_lt line 34

Source documentation

The terminal normalized residue condition gives a genuine power-saving integer residue step, including the case of residue zero.

lemma terminal_step_of_fract_lt {t u : ℕ} {η : ℝ}
    (ht : 0 < t) (hu : 0 < u)
    (hsmall : Int.fract (-(t : ℝ) / u) < (u : ℝ) ^ (-η)) :
    ∃ z h : ℕ, 0 < z ∧ (h : ℝ) ≤ (u : ℝ) ^ (1 - η) ∧
      t + h = u * z := by
…

abbrev OAI.Problem337.GeometricDensity.depth line 55
abbrev OAI.Problem337.GeometricDensity.cutoff line 58
abbrev OAI.Problem337.GeometricDensity.factor line 61
abbrev OAI.Problem337.GeometricDensity.contraction line 64
structure OAI.Problem337.GeometricDensity.NormalizedResidueData line 70
Source documentation
Arithmetic residue information on the canonical geometric levels. The normalized Fourier conclusion, exceptional count, shifted-divisor moment, and terminal shrinking residue remain explicit hypotheses. All geometric alignment, ceiling equations, and expansion construction are supplied below.
```
structure NormalizedResidueData (DM D₀ η c r S loss : ℝ) (C M : ℕ) where
…
```
structure OAI.Problem337.GeometricDensity.ResidueData line 97
Source documentation
The weaker, directly consumable arithmetic data: only actual ceiling residues are bounded. In particular a non-strict residue bound is sufficient.
```
structure ResidueData (DM D₀ η c r S loss : ℝ) (C M : ℕ) where
…
```
def OAI.Problem337.GeometricDensity.NormalizedResidueData.toResidueData line 124
Source documentation
A normalized strict discrepancy conclusion implies the weaker ceiling residue interface, without demanding a strict inequality from later consumers.
```
def NormalizedResidueData.toResidueData {DM D₀ η c r S loss : ℝ} {C M : ℕ}
    (H : NormalizedResidueData DM D₀ η c r S loss C M) (hS : 0 < S) :
    ResidueData DM D₀ η c r S loss C M := by
…
```
Mentions: OAI.Problem337.GeometricDensity.NormalizedResidueData, OAI.Problem337.GeometricDensity.ResidueData

def OAI.Problem337.GeometricDensity.ResidueData.toFamily line 168

Source documentation

Construct the exact raw family from ceiling residue information at the canonical levels. This definition discharges every ceiling, divisibility, terminal-expansion, and geometric-transition field.

def ResidueData.toFamily {DM D₀ η c r S loss : ℝ} {C M : ℕ}
    (H : ResidueData DM D₀ η c r S loss C M)
    (hDM : 1 < DM) (hD₀ : 1 ≤ D₀) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
    (hS : 1 ≤ S) (hlog : 1 ≤ Real.log S) (hscale : 2 ≤ ResidueLevels.scale S)
    (hC : 0 < C) (hM : Real.exp S < (M : ℝ))
    (hbinary : 2 ^ TerminalDepth.binaryExponent D₀ S ∣ M)
    (hloss : 0 < loss)
    (hloss_bound : 1 + loss * Real.exp (S ^ (1 / 4 : ℝ) / r) ≤
      Real.exp (2 * S ^ (1 / 4 : ℝ))) :
    DensityResidueFamily S (ResidueLevels.scale S) (contraction η S) r c
      (depth DM η S) := by
…

Mentions: OAI.Problem337.GeometricDensity.ResidueData, OAI.Problem337.ResidueLevels.scale, OAI.Problem337.TerminalDepth.binaryExponent, OAI.Problem337.DensityResidueFamily, OAI.Problem337.GeometricDensity.contraction, OAI.Problem337.GeometricDensity.depth

theorem OAI.Problem337.GeometricDensity.raw_density_supply_of_geometric_residues line 249

Source documentation

The concrete geometric construction meets the raw upper-bound interface. Only the arithmetic input data, denominator size, and the displayed loss estimate are assumed; the depth and rounded terminal length are proved.

theorem raw_density_supply_of_geometric_residues
    {DM D₀ η c r S loss : ℝ} {C M : ℕ}
    (H : ResidueData DM D₀ η c r S loss C M)
    (hDM : 1 < DM) (hD₀ : 1 ≤ D₀) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
    (hS : 1 ≤ S) (hlog : 1 ≤ Real.log S) (hscale : 2 ≤ ResidueLevels.scale S)
    (hscale_lower : S / (2 * Real.log S) ≤ (ResidueLevels.scale S : ℝ))
    (hC : 0 < C) (hM : Real.exp S < (M : ℝ))
    (hMupper : (M : ℝ) ≤ Real.exp (DM * S))
    (hbinary : 2 ^ TerminalDepth.binaryExponent D₀ S ∣ M)
    (hloss : 0 < loss)
    (hloss_bound : 1 + loss * Real.exp (S ^ (1 / 4 : ℝ) / r) ≤
      Real.exp (2 * S ^ (1 / 4 : ℝ))) :
…

Mentions: OAI.Problem337.GeometricDensity.ResidueData, OAI.Problem337.ResidueLevels.scale, OAI.Problem337.TerminalDepth.binaryExponent