Parameters.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Parameters fixed before the prime is chosen

These are the literal accuracy, pivot-slot, direction-count and encoding-cost parameters of the construction. The radius and rank are genuinely available for every proposed comparison constant. Their existence does not depend on the eventual field size.

def OAI.MetricEntropyDuality.accuracy line 24
def OAI.MetricEntropyDuality.pivotSlots line 26
def OAI.MetricEntropyDuality.compressionRadius line 29
Source documentation
A fixed positive radius satisfying the logarithmic compression condition.
```
def compressionRadius (a : ℝ) : ℕ :=
…
```
def OAI.MetricEntropyDuality.directionCount line 32
def OAI.MetricEntropyDuality.encodingCost line 35
theorem OAI.MetricEntropyDuality.accuracy_pos line 39
theorem OAI.MetricEntropyDuality.accuracy_lt_one line 44
theorem OAI.MetricEntropyDuality.accuracy_cover_scale line 49
theorem OAI.MetricEntropyDuality.one_div_le_pivotSlots line 58
theorem OAI.MetricEntropyDuality.pivotSlots_pos line 61
theorem OAI.MetricEntropyDuality.one_le_mul_pivotSlots line 65
theorem OAI.MetricEntropyDuality.compressionRadius_pos line 70
theorem OAI.MetricEntropyDuality.compressionRadius_log_pos line 73
theorem OAI.MetricEntropyDuality.compressionRadius_log_le line 79
theorem OAI.MetricEntropyDuality.exists_rank line 93
Source documentation
The rank can be chosen after the compression parameters and before the prime.
```
theorem exists_rank (b θ : ℝ) {h : ℕ} (hh : 0 < h) :
    ∃ r : ℕ, 0 < r ∧
      8 * b * (h : ℝ) ^ 2 * (pivotSlots θ : ℝ) < (r : ℝ) + h - 1 := by
…
```
Mentions: OAI.MetricEntropyDuality.pivotSlots
theorem OAI.MetricEntropyDuality.directionCount_pos line 103
theorem OAI.MetricEntropyDuality.directionCount_budget line 112
Source documentation
The natural ceiling has exactly the direction needed by the deletion argument.
```
theorem directionCount_budget {r h : ℕ} {θ : ℝ} (hθ : 0 < θ) :
    (h : ℝ) * (2 * (formDimension r h : ℝ)) ≤ θ * (directionCount r h θ : ℝ) := by
…
```
Mentions: OAI.MetricEntropyDuality.formDimension, OAI.MetricEntropyDuality.directionCount
theorem OAI.MetricEntropyDuality.encodingCost_pos line 119

theorem OAI.MetricEntropyDuality.exists_parameters line 133

Source documentation

Simultaneous scalar choices, with all dependent quantities already fixed.

theorem exists_parameters {a : ℝ} (ha : 1 ≤ a) (b : ℝ) :
    ∃ h r : ℕ, h = compressionRadius a ∧ 0 < h ∧ 0 < r ∧
      Real.log 3 / Real.log ((h : ℝ) + 1) ≤ accuracy a ∧
      8 * b * (h : ℝ) ^ 2 * (pivotSlots (accuracy a) : ℝ) < (r : ℝ) + h - 1 ∧
      0 < formDimension r h ∧
      0 < directionCount r h (accuracy a) ∧
      (h : ℝ) * (2 * (formDimension r h : ℝ)) ≤
        accuracy a * (directionCount r h (accuracy a) : ℝ) ∧
      0 < encodingCost h (accuracy a) (directionCount r h (accuracy a)) := by
…

Mentions: OAI.MetricEntropyDuality.compressionRadius, OAI.MetricEntropyDuality.accuracy, OAI.MetricEntropyDuality.pivotSlots, OAI.MetricEntropyDuality.formDimension, OAI.MetricEntropyDuality.directionCount, OAI.MetricEntropyDuality.encodingCost