UniformNormalization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ParityWL.Complexity.uniform_eth_unrestricted_exponents line 9
Source documentation
Nonnegative exponents and positive multipliers in UniformWLBound are a normalization, not an added restriction on uniform exclusion.
```
theorem uniform_eth_unrestricted_exponents (hETH : UniformSubexponentialETH)
    (c : Convention) (i : Implementation) :
    ¬ ∃ (M : Machine) (f g : ℕ → ℝ),
      Filter.Tendsto (fun k : ℕ => g k/k) Filter.atTop (nhds 0) ∧
      ∀ k : ℕ, 4 ≤ k → ∀ (n : ℕ) (G H : SimpleGraph (Fin n)), ∃ s b,
        Emits M (encodeNat k++encodeGraphs G H) s b ∧
        (b=true↔Equivalent G H c i k) ∧ (s : ℝ) ≤ f k*(n+1 : ℝ)^g k := by
…
```
Mentions: OAI.ParityWL.Complexity.UniformSubexponentialETH, OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation, OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Complexity.Emits, OAI.ParityWL.Complexity.encodeNat, OAI.ParityWL.Complexity.encodeGraphs, OAI.ParityWL.Complexity.Equivalent