AsymptoticBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ParityWL.Complexity.extend_wl_time_bound line 9

Source documentation

Finite exceptional orders do not change a time bound for a total decider. The bound is on actual executions, and no effective choice of constants is needed.

lemma extend_wl_time_bound (M : Machine) (header : List Bool) (c : Convention)
    (i : Implementation) (k : ℕ) (r C : ℝ) (hr : 0 ≤ r) (hC : 0<C) (N₀ : ℕ)
    (hTotal : ∀ n : ℕ, ∀ G H : SimpleGraph (Fin n), ∃ s b,
      Emits M (header++encodeGraphs G H) s b ∧ (b=true↔Equivalent G H c i k))
    (hLarge : ∀ n : ℕ, N₀ ≤ n → ∀ G H : SimpleGraph (Fin n), ∃ s b,
      Emits M (header++encodeGraphs G H) s b ∧ (b=true↔Equivalent G H c i k) ∧
      (s : ℝ) ≤ C*(n+1 : ℝ)^r) :
    ∃ D : ℝ, 0<D ∧ ∀ n : ℕ, ∀ G H : SimpleGraph (Fin n), ∃ s b,
      Emits M (header++encodeGraphs G H) s b ∧ (b=true↔Equivalent G H c i k) ∧
      (s : ℝ) ≤ D*(n+1 : ℝ)^r := by
…

Mentions: OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation, OAI.ParityWL.Complexity.Emits, OAI.ParityWL.Complexity.encodeGraphs, OAI.ParityWL.Complexity.Equivalent

def OAI.ParityWL.Complexity.AsymptoticFixedWLBound line 43
Source documentation
The conventional big-O form: total correctness and one eventual n^r bound. This allows arbitrary behavior at the finitely many smaller graph orders.
```
noncomputable def AsymptoticFixedWLBound (M : Machine) (c : Convention)
    (i : Implementation) (k : ℕ) (r : ℝ) : Prop :=
…
```
Mentions: OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation
lemma OAI.ParityWL.Complexity.AsymptoticFixedWLBound.fixed line 52
theorem OAI.ParityWL.Complexity.fixed_dimension_eth_asymptotic line 66
Source documentation
O(n^(c*k)) exclusion, with arbitrary finite exceptional orders.
```
theorem fixed_dimension_eth_asymptotic (hETH : PositiveRateETH) :
    ∃ c : ℝ, 0<c ∧ ∃ K : ℕ, 4 ≤ K ∧ ∀ k : ℕ, K ≤ k →
      ∀ conv : Convention, ∀ i : Implementation,
        ¬ ∃ M : Machine, AsymptoticFixedWLBound M conv i k (c*k) := by
…
```
Mentions: OAI.ParityWL.Complexity.PositiveRateETH, OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation, OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Complexity.AsymptoticFixedWLBound
def OAI.ParityWL.Complexity.AsymptoticUniformWLBound line 78
Source documentation
Eventual time bounds may start at an arbitrary order depending on k; the same finite machine receives binary k and the two full adjacency matrices.
```
noncomputable def AsymptoticUniformWLBound (M : Machine) (c : Convention)
    (i : Implementation) (f g : ℕ → ℝ) : Prop :=
…
```
Mentions: OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation
theorem OAI.ParityWL.Complexity.uniform_eth_asymptotic line 90
Source documentation
Uniform exclusion, even with arbitrary finite exceptions and without any sign assumptions on f or g. No computable modulus is required.
```
theorem uniform_eth_asymptotic (hETH : UniformSubexponentialETH)
    (c : Convention) (i : Implementation) :
    ¬ ∃ (M : Machine) (f g : ℕ → ℝ),
      Filter.Tendsto (fun k : ℕ => g k/k) Filter.atTop (nhds 0) ∧
      AsymptoticUniformWLBound M c i f g := by
…
```
Mentions: OAI.ParityWL.Complexity.UniformSubexponentialETH, OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation, OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Complexity.AsymptoticUniformWLBound