OAI/NumberTheory/Ostmann/Arithmetic/PrimePatternUniformBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equality-pattern costs for two prime giants

  1. theorem OAI.Ostmann.movingPattern_prime_loss_le line 10
  2. theorem OAI.Ostmann.movingPattern_prime_error_sum_le line 23

    Source documentation

    Summing every original equality pattern introduces only a depth-dependent factor. The number of protected bulk slots never appears in this cost.

    theorem movingPattern_prime_error_sum_le (n : ℕ) (E D : ℝ) (hE : 0 ≤ E) (hD : 0 ≤ D) :
    letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
…

    Mentions: OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex