ResidueLevels.lean`

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ResidueLevels.depth line 11
Source documentation
The first index at which a geometric scale reaches exp m.
```
def depth (A m η : ℝ) : ℕ := ⌈(A - m) / (η * m)⌉₊
```
def OAI.Problem337.ResidueLevels.level line 14
Source documentation
A geometric scale, kept in logarithmic coordinates.
```
def level (A m η : ℝ) (j : ℕ) : ℝ := Real.exp (A - η * m * j)
```
theorem OAI.Problem337.ResidueLevels.before_depth_iff line 16
theorem OAI.Problem337.ResidueLevels.depth_pos line 21
theorem OAI.Problem337.ResidueLevels.level_pos line 26
theorem OAI.Problem337.ResidueLevels.level_strictAnti line 29
theorem OAI.Problem337.ResidueLevels.level_above_cutoff line 37
theorem OAI.Problem337.ResidueLevels.final_level_bounds line 41
theorem OAI.Problem337.ResidueLevels.half_log_le_next line 60
theorem OAI.Problem337.ResidueLevels.exp_half_le_next line 68
theorem OAI.Problem337.ResidueLevels.sqrt_level_le_next line 73
theorem OAI.Problem337.ResidueLevels.depth_upper line 83
theorem OAI.Problem337.ResidueLevels.depth_log_bound line 94
def OAI.Problem337.ResidueLevels.factor line 119
Source documentation
The auxiliary denominator factor changes only from C to 1.
```
def factor (A m η S : ℝ) (C j : ℕ) : ℕ :=
…
```
theorem OAI.Problem337.ResidueLevels.next_factor_dvd line 122
def OAI.Problem337.ResidueLevels.scale line 133
Source documentation
The integer number of prime factors used at scale S.
```
def scale (S : ℝ) : ℕ := ⌊S / Real.log S⌋₊
```
theorem OAI.Problem337.ResidueLevels.tendsto_div_log line 135
theorem OAI.Problem337.ResidueLevels.scale_bounds line 150
theorem OAI.Problem337.ResidueLevels.eventually_scale_bounds line 164
theorem OAI.Problem337.ResidueLevels.tendsto_scale line 174
theorem OAI.Problem337.ResidueLevels.tendsto_div_scale line 180
theorem OAI.Problem337.ResidueLevels.eventually_depth_log_bound line 189
theorem OAI.Problem337.ResidueLevels.eventually_exp_absorb line 204
Source documentation
An error exponential in S is negligible beside any fixed exponential in the smaller prime-product scale.
```
theorem eventually_exp_absorb {a b c C : ℝ} (hab : a < b) (hc : 0 < c)
    (hC : 0 ≤ C) : ∀ᶠ S : ℝ in atTop,
    Real.exp (-b * scale S) + C * Real.exp (-c * S) ≤
      Real.exp (-a * scale S) := by
…
```
Mentions: OAI.Problem337.ResidueLevels.scale
theorem OAI.Problem337.ResidueLevels.eventually_deterministic_mean_bound line 248
theorem OAI.Problem337.ResidueLevels.level_zero line 259
theorem OAI.Problem337.ResidueLevels.level_succ line 262
theorem OAI.Problem337.ResidueLevels.final_factor_one line 268
theorem OAI.Problem337.ResidueLevels.exists_interval_index line 278
Source documentation
Finite adjacent descending intervals cover the region between the endpoints. No continuity or integrality of interval endpoints is required.
```
theorem exists_interval_index {f : ℕ → ℝ} {d : ℕ} {u : ℝ}
    (hlo : f d < u) (hhi : u ≤ f 0) :
    ∃ j : ℕ, j < d ∧ f (j + 1) < u ∧ u ≤ f j := by
…
```
theorem OAI.Problem337.ResidueLevels.interval_index_unique line 289
theorem OAI.Problem337.ResidueLevels.exists_unique_level_interval line 302
theorem OAI.Problem337.ResidueLevels.factor_pos line 312
Source documentation
Every auxiliary factor is positive once the initial factor is.
```
theorem factor_pos {A m η S : ℝ} {C : ℕ} (hC : 0 < C) (j : ℕ) :
    0 < factor A m η S C j := by
…
```
Mentions: OAI.Problem337.ResidueLevels.factor
theorem OAI.Problem337.ResidueLevels.factor_le line 317
theorem OAI.Problem337.ResidueLevels.factor_zero line 322
theorem OAI.Problem337.ResidueLevels.factor_eq_of_large_numerator line 327
theorem OAI.Problem337.ResidueLevels.scale_le_self line 334
Source documentation
The floor scale lies below the original scale; this is the missing comparison needed to certify that the terminal auxiliary factor equals one.
```
theorem scale_le_self {S : ℝ} (hS : 0 ≤ S) (hlog : 1 ≤ Real.log S) :
    (scale S : ℝ) ≤ S := by
…
```
Mentions: OAI.Problem337.ResidueLevels.scale