Powers.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.samplingQ line 11
def OAI.FiniteFactor.samplingH line 12
def OAI.FiniteFactor.samplingR line 13
theorem OAI.FiniteFactor.sampling_integer_candidates line 15
theorem OAI.FiniteFactor.sampling_forbidden_budget line 29

theorem OAI.FiniteFactor.exists_source_sampling_powers line 53

Source documentation

An explicit sufficiently-large threshold discharges the source's greedy asymptotics, retaining Q, H, R and the exponent 0.69m exactly.

theorem exists_source_sampling_powers (m K : ℕ) (hm : 200000 ≤ m) (hK : K ≤ m) :
    ∃ N : Finset ℤ,
      (∀ n ∈ N, samplingQ m/2 ≤ (n : ℝ) ∧ (n : ℝ) ≤ samplingQ m ∧ 0 < n) ∧
      (m : ℝ)^((69/100 : ℝ)*(m : ℝ)) ≤ (N.card : ℝ) ∧
      (N : Set ℤ).Pairwise (fun n n' => ¬SamplingConflict (samplingH m) (samplingR m K) n n') := by
…

Mentions: OAI.FiniteFactor.samplingQ, OAI.FiniteFactor.SamplingConflict, OAI.FiniteFactor.samplingH, OAI.FiniteFactor.samplingR

def OAI.FiniteFactor.sourceSamplingPowers line 119
Source documentation
A deterministic finite set fixed from the numerical stages alone.
```
def sourceSamplingPowers (s : ℕ) : Finset ℤ :=
…
```
theorem OAI.FiniteFactor.sourceSamplingPowers_spec line 125
theorem OAI.FiniteFactor.sourceSamplingPowers_eventually line 138