WeightedQuadraticLift.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted quadratic witnesses supply the common-center lifts

theorem OAI.Ostmann.weighted_quadratic_phase_witness line 14

Source documentation

Multiplying the inverse denominator by the actual quadratic coefficient produces precisely the phase witness used by the common-center argument.

theorem weighted_quadratic_phase_witness (w : ℕ → ℂ) (β δ : ℝ)
    (N c Amax : ℕ) (θ : ℝ) (hN : 0 < N) (hc : 0 < c)
    (hδ : 0 < δ) (hδ1 : δ ≤ 1)
    (hscale : 512 * (1 + 2 * Real.log (N : ℝ)) ≤ δ ^ 3 * N)
    (hlarge : discreteVariation w N * (δ * N) <
      ‖∑ j ∈ Finset.range N, w j * realQuadraticPhase ((c : ℝ) * θ) β j‖)
    (hA : 1024 * (c : ℝ) / δ ^ 2 ≤ Amax) :
    ∃ a ∈ Finset.Icc 1 Amax, ∃ b : ℤ,
      |(a : ℝ) * θ - b| ≤
        1024 * (1 + 2 * Real.log (N : ℝ)) / (δ ^ 4 * (N : ℝ) ^ 2) := by
…

Mentions: OAI.Ostmann.discreteVariation, OAI.Ostmann.realQuadraticPhase

theorem OAI.Ostmann.weighted_quadratic_tuple_lift line 43

Source documentation

With the already constructed tuple residue and product modulus, the weighted witness gives the bounded simultaneous integer lift.

theorem weighted_quadratic_tuple_lift (P : Finset ℕ) (hprime : ∀ p ∈ P, p.Prime)
    {k : ℕ} (e : Fin k ↪ P) (w : ℕ → ℂ) (β δ : ℝ)
    (N c Amax H : ℕ) (tM : ℤ) (t : ℕ → ℤ)
    (hN : 0 < N) (hc : 0 < c) (hδ : 0 < δ) (hδ1 : δ ≤ 1)
    (hscale : 512 * (1 + 2 * Real.log (N : ℝ)) ≤ δ ^ 3 * N)
    (hlarge : discreteVariation w N * (δ * N) <
      ‖∑ j ∈ Finset.range N, w j *
        realQuadraticPhase ((c : ℝ) * ((tM : ℝ) / primeTupleProduct P e)) β j‖)
    (hA : 1024 * (c : ℝ) / δ ^ 2 ≤ Amax)
    (hH : (primeTupleProduct P e : ℝ) *
      (1024 * (1 + 2 * Real.log (N : ℝ)) / (δ ^ 4 * (N : ℝ) ^ 2)) ≤ H)
    (ht : ∀ i, ((e i).1 : ℤ) ∣ tM - t (e i).1) :
…

Mentions: OAI.Ostmann.discreteVariation, OAI.Ostmann.realQuadraticPhase, OAI.Ostmann.primeTupleProduct