ParameterEstimates.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Compatible parameters and elementary asymptotics

The strict inequalities here are the weight margins of arithmetic.tex. The subsequent limits account for the sampling entropy and the logarithmic factors in the prime cutoff and amplification parameters.

def OAI.JointDickman.weightBaseExponent line 20
def OAI.JointDickman.weightExponent line 22
def OAI.JointDickman.samplingTau line 25
Source documentation
One concrete choice satisfying all three weight margins.
```
noncomputable def samplingTau : ℝ := 1 / 1000
```
def OAI.JointDickman.amplificationExponent line 27
theorem OAI.JointDickman.samplingTau_pos line 29
theorem OAI.JointDickman.weightBaseExponent_pos line 31
theorem OAI.JointDickman.amplificationExponent_gt_one line 36
theorem OAI.JointDickman.weightExponent_mono line 41
theorem OAI.JointDickman.samplingTau_weight_margins line 48

theorem OAI.JointDickman.weight_margins_of_le_samplingTau line 60

Source documentation

Every smaller nonnegative tolerance preserves the strict margins.

theorem weight_margins_of_le_samplingTau {τ : ℝ} (hτ : τ ≤ samplingTau) :
    2 * weightExponent τ < (32 / 100 : ℝ) ∧
      (7 / 100 : ℝ) < 1 - 6 * weightExponent τ ∧
      (229 / 1000 : ℝ) < 1 - 5 * weightExponent τ := by
…

Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.weightExponent

theorem OAI.JointDickman.power_mul_log_isLittleO line 72
Source documentation
A fixed power times a logarithm is smaller than any strictly larger power. The base tends through positive reals.
```
theorem power_mul_log_isLittleO {a b : ℝ} (hab : a < b) :
    (fun B : ℝ => B ^ a * Real.log B) =o[atTop] (fun B => B ^ b) := by
…
```
theorem OAI.JointDickman.power_mul_log_div_power_tendsto_zero line 83
theorem OAI.JointDickman.sampling_entropy_isLittleO line 88

theorem OAI.JointDickman.exp_power_log_sub_power_tendsto_zero line 95

Source documentation

The union-bound entropy is absorbed by the negative concentration exponent whenever the latter has a strictly larger positive power.

theorem exp_power_log_sub_power_tendsto_zero {a b c : ℝ}
    (hab : a < b) (hb : 0 < b) (hc : 0 < c) (C : ℝ) :
    Tendsto (fun B : ℝ => Real.exp (C * (B ^ a * Real.log B) - c * B ^ b))
      atTop (𝓝 0) := by
…

theorem OAI.JointDickman.sampling_union_bound_tendsto_zero line 110
theorem OAI.JointDickman.power_div_power_tendsto_zero line 117
Source documentation
Every smaller real power is negligible compared with a larger one.
```
theorem power_div_power_tendsto_zero {a b : ℝ} (hab : a < b) :
    Tendsto (fun B : ℝ => B ^ a / B ^ b) atTop (𝓝 0) := by
…
```
theorem OAI.JointDickman.polynomial_div_primeCutoff_tendsto_zero line 128
Source documentation
In particular, each fixed polynomial degree below the cutoff exponent is negligible compared with P₀ = B^1000.
```
theorem polynomial_div_primeCutoff_tendsto_zero {k : ℕ} (hk : k < 1000) :
    Tendsto (fun B : ℝ => B ^ k / B ^ (1000 : ℕ)) atTop (𝓝 0) := by
…
```
theorem OAI.JointDickman.log_power_div_power_tendsto_zero line 137
Source documentation
Fixed logarithmic powers are smaller than every positive real power.
```
theorem log_power_div_power_tendsto_zero (r : ℝ) {s : ℝ} (hs : 0 < s) :
    Tendsto (fun B : ℝ => (Real.log B) ^ r / B ^ s) atTop (𝓝 0) :=
…
```
theorem OAI.JointDickman.amplification_log_loss_tendsto_zero line 143
Source documentation
The amplification loss B/R^α, with R=B/(1000 log B), vanishes for every α>1. This is the exact expression before introducing R.
```
theorem amplification_log_loss_tendsto_zero {α : ℝ} (hα : 1 < α) :
    Tendsto (fun B : ℝ => B * (1000 * Real.log B) ^ α / B ^ α)
      atTop (𝓝 0) := by
…
```
theorem OAI.JointDickman.amplification_log_loss line 158