OAI/NumberTheory/TwoPoint/Walks/ProhibitedCostComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positive costs at actual prohibited sites. The forbidden-word DNF is conjoined with the padding divisor test on a shared list of prime literals; all circuit bounds are derived here.

  1. def OAI.TwoPointCorrelations.prohibitedCostCircuit line 16
  2. lemma OAI.TwoPointCorrelations.prohibitedCostCircuit_eval line 21
  3. lemma OAI.TwoPointCorrelations.prohibitedCostCircuit_depth line 33
  4. lemma OAI.TwoPointCorrelations.prohibitedCostCircuit_size line 42
  5. lemma OAI.TwoPointCorrelations.prohibitedCostCircuit_size_exp line 52
  6. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_prohibited_cost_comparison line 77

    Source documentation

    One actual positive tuple/padding cost at a prohibited origin is compared with its value under the same residue law as the graph.

    theorem BravermanDepth22Input.eventually_prohibited_cost_comparison
    (hBr : BravermanDepth22Input) :
    ∃ A : ℕ, 1000 ≤ A ∧ ∀ᶠ L : ℝ in atTop,
      ∀ (h J M B s cap : ℕ) (data : ProhibitedPrimeFamily h J M)
        (hB : ∀ p ∈ data.P ∪ data.Q, p ≤ B),
      (data.P ∪ data.Q).Nonempty → (B : ℝ) ≤ Real.exp L →
      (s : ℝ) ≤ L → (cap : ℝ) ≤ L ^ 2 →
      (data.pairs.card : ℝ) ≤ Real.exp (101 * L) →
      (∀ dq ∈ data.pairs, (dq.2 * dq.1).primeFactors.card ≤ cap) →
      ∀ (S : Finset ℕ), S ⊆ data.P ∪ data.Q → (S.card : ℝ) ≤ L ^ 2 →
      ∀ (q : ℕ), q ∈ retainedPrimeDivisors data.Q →
      (q.primeFactors.card : ℝ) ≤ 100 * Real.log L →
…

    Mentions: OAI.TwoPointCorrelations.BravermanDepth22Input, OAI.TwoPointCorrelations.ProhibitedPrimeFamily, OAI.TwoPointCorrelations.retainedPrimeDivisors