RunWeights.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Analytic weight estimates for the D-runs in the path-type sum.

lemma OAI.Problem335.RunWeights.interval_weight_le line 13

Source documentation

The interval discrepancy estimate converts directly into a bound on its weight.

lemma interval_weight_le {α β ρ ε N : ℝ} (hα : 0 < α) (hα1 : α ≤ 1)
    (hβ : 0 ≤ β) (hβupper : β ≤ α ^ ρ * Real.exp ε)
    (hscale : α ^ (-(1 + ρ)) ≤ N) (v u : ℕ)
    (hdiscrepancy : (v : ℝ) - ρ * u ≤ 1 + ρ) :
    α ^ (-(v : ℝ)) * β ^ u ≤ N * Real.exp (ε * u) := by
…

lemma OAI.Problem335.RunWeights.scale_le_of_inv_le_sqrt line 34

Source documentation

The parameter bound on alpha controls the common cost of every run.

lemma scale_le_of_inv_le_sqrt {α ρ N : ℝ} (hα : 0 < α) (hα1 : α ≤ 1)
    (hρ : ρ ≤ 1) (hN : 0 ≤ N) (hinv : α⁻¹ ≤ Real.sqrt N) :
    α ^ (-(1 + ρ)) ≤ N := by
…

lemma OAI.Problem335.RunWeights.interval_weight_le_of_inv_le_sqrt line 46

lemma OAI.Problem335.RunWeights.prod_interval_weight_le line 56

Source documentation

Multiplying the run estimates accumulates only their total number of U layers.

lemma prod_interval_weight_le {ι : Type*} (S : Finset ι) {α β ρ ε N : ℝ}
    (hα : 0 < α) (hα1 : α ≤ 1) (hβ : 0 ≤ β)
    (hβupper : β ≤ α ^ ρ * Real.exp ε) (hscale : α ^ (-(1 + ρ)) ≤ N)
    (v u : ι → ℕ) (hdiscrepancy : ∀ i ∈ S, (v i : ℝ) - ρ * u i ≤ 1 + ρ) :
    (∏ i ∈ S, α ^ (-(v i : ℝ)) * β ^ u i) ≤
      N ^ S.card * Real.exp (ε * ∑ i ∈ S, (u i : ℝ)) := by
…

lemma OAI.Problem335.RunWeights.one_add_pow_le_exp line 74

lemma OAI.Problem335.RunWeights.correction_prefactor_le_exp line 81

Source documentation

The isolated-position correction prefactor costs at most exp(3 sqrt N).

lemma correction_prefactor_le_exp {N a : ℝ} (hN : 1 ≤ N)
    (ha : 0 ≤ a) (haN : a ≤ Real.sqrt N) (k : ℕ) (hk : 2 * (k : ℝ) ≤ N) :
    (1 + 2 / N ^ 2) ^ k * (1 + a) * (1 + a / N) ^ k ≤
      Real.exp (3 * Real.sqrt N) := by
…

lemma OAI.Problem335.RunWeights.u_correction_le_exp line 111

Source documentation

Pointwise U-layer corrections cost at most exp(2 sqrt N).

lemma u_correction_le_exp {N β : ℝ} (hN : 0 < N) (hβ : 0 ≤ β)
    (hβN : β ≤ 2 / Real.sqrt N) (m : ℕ) (hm : (m : ℝ) ≤ N) :
    (1 + β) ^ m ≤ Real.exp (2 * Real.sqrt N) := by
…

lemma OAI.Problem335.RunWeights.correction_product_le line 125

Source documentation

Surviving N-layers have a small correction, except possibly at one endpoint.

lemma correction_product_le {ι : Type*} [DecidableEq ι] (T : Finset ι)
    (e : ι) (h : ι → ℕ) {N a : ℝ} (hN : 1 ≤ N) (ha : 0 ≤ a)
    (k : ℕ) (hcard : T.card ≤ k)
    (hinterior : ∀ i ∈ T, i ≠ e → 1 ≤ h i) :
    (∏ i ∈ T, (1 + a * (N⁻¹) ^ h i)) ≤ (1 + a) * (1 + a / N) ^ k := by
…