GeometricRandomRanges.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.GeometricRandomRanges.cutoff line 10
Source documentation
The common geometric cutoffs used in the random middle-level selection.
```
def cutoff (D S : ℝ) (j : ℕ) : ℝ :=
…
```
Mentions: OAI.Problem337.D
def OAI.Problem337.GeometricRandomRanges.middleTests line 14
Source documentation
Only levels whose denominator factor is one need a random block.
```
def middleTests (D S : ℝ) : Finset ℕ :=
…
```
Mentions: OAI.Problem337.D
def OAI.Problem337.GeometricRandomRanges.middleLevel line 19
Source documentation
Positive integers in the open-closed interval between adjacent cutoffs.
```
def middleLevel (D S : ℝ) (j : ℕ) : Finset ℕ :=
…
```
Mentions: OAI.Problem337.D
def OAI.Problem337.GeometricRandomRanges.terminalRange line 24
Source documentation
The terminal numerators not covered by the binary factor.
```
def terminalRange (S : ℝ) : Finset ℕ :=
…
```
theorem OAI.Problem337.GeometricRandomRanges.eventually_log_mul_le_scale line 31
Source documentation
The floor prime-product scale eventually dominates any fixed multiple of log S. This simultaneously handles the number of levels and the random product theorem's lower logarithmic cutoff.
```
theorem eventually_log_mul_le_scale (K : ℝ) :
    ∀ᶠ S : ℝ in atTop, K * Real.log S ≤ (ResidueLevels.scale S : ℝ) := by
…
```
Mentions: OAI.Problem337.ResidueLevels.scale
theorem OAI.Problem337.GeometricRandomRanges.mem_middleTests line 50
theorem OAI.Problem337.GeometricRandomRanges.mem_middleLevel line 55
theorem OAI.Problem337.GeometricRandomRanges.middleLevel_card_le line 63
theorem OAI.Problem337.GeometricRandomRanges.middle_log_bounds line 73
Source documentation
The exact logarithmic window, including the slight overlap of the middle level with numerators below exp m.
```
theorem middle_log_bounds {D S : ℝ}
    (hm : 0 < (ResidueLevels.scale S : ℝ)) {j u : ℕ}
    (hj : j ∈ middleTests D S) (hu : u ∈ middleLevel D S j) :
    (9999 / 10000 : ℝ) * (ResidueLevels.scale S : ℝ) < Real.log (u : ℝ) ∧
      Real.log (u : ℝ) ≤ S := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.ResidueLevels.scale, OAI.Problem337.GeometricRandomRanges.middleTests, OAI.Problem337.GeometricRandomRanges.middleLevel
theorem OAI.Problem337.GeometricRandomRanges.mem_terminalRange line 93
theorem OAI.Problem337.GeometricRandomRanges.terminal_log_bounds line 102
Source documentation
The terminal range has exactly the log window required by random products.
```
theorem terminal_log_bounds {S : ℝ} (hS : 0 < S) {u : ℕ}
    (hu : u ∈ terminalRange S) :
    100000 * Real.log S < Real.log (u : ℝ) ∧
      Real.log (u : ℝ) ≤ (ResidueLevels.scale S : ℝ) := by
…
```
Mentions: OAI.Problem337.GeometricRandomRanges.terminalRange, OAI.Problem337.ResidueLevels.scale
structure OAI.Problem337.GeometricRandomRanges.SelectionRanges line 116
Source documentation
All non-arithmetic hypotheses of the common sampled-Fourier selection, for the actual geometric middle levels and terminal interval. The finite indices retain multiplicity; no residue or cancellation bound is assumed.
```
structure SelectionRanges (D S : ℝ) (N : ℕ) : Prop where
…
```
Mentions: OAI.Problem337.D
theorem OAI.Problem337.GeometricRandomRanges.eventually_selectionRanges line 133
Source documentation
A single onset works for all middle levels and terminal numerators. In particular the abstract random-selection range premises are satisfied by the explicit geometric cutoffs, not assumed separately.
```
theorem eventually_selectionRanges (D : ℝ) (hD : 1 ≤ D) (N : ℕ) :
    ∀ᶠ S : ℝ in atTop, SelectionRanges D S N := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.GeometricRandomRanges.SelectionRanges
theorem OAI.Problem337.GeometricRandomRanges.mem_middleLevel_iff line 170
Source documentation
Characterization for applying a selected finite-level conclusion to an arbitrary integer in the geometric interval.
```
theorem mem_middleLevel_iff {D S : ℝ} {j u : ℕ} :
    u ∈ middleLevel D S j ↔
      0 < u ∧ cutoff D S (j + 1) < (u : ℝ) ∧ (u : ℝ) ≤ cutoff D S j := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.GeometricRandomRanges.middleLevel, OAI.Problem337.GeometricRandomRanges.cutoff
theorem OAI.Problem337.GeometricRandomRanges.mem_terminalRange_iff line 180
Source documentation
Characterization for applying the terminal conclusion outside the binary range. It retains the open lower endpoint and the closed upper endpoint.
```
theorem mem_terminalRange_iff {S : ℝ} {u : ℕ} :
    u ∈ terminalRange S ↔ 0 < u ∧ S ^ 100000 < (u : ℝ) ∧
      (u : ℝ) ≤ Real.exp (ResidueLevels.scale S) := by
…
```
Mentions: OAI.Problem337.GeometricRandomRanges.terminalRange, OAI.Problem337.ResidueLevels.scale
theorem OAI.Problem337.GeometricRandomRanges.mem_middleTests_iff line 188