MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryOddPrimePowerStationary

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_localization (p m : ℕ) [NeZero p] [NeZero m] (a d : ℤ) :

completeKloosterman (p * (m * m)) (↑a) d = ∑ u : ZMod (p * (m * m)), if IsUnit u ∧ ↑a * (ZMod.castHom ⋯ (ZMod m)) u ^ 2 = ↑d then ZMod.stdAddChar (↑a * u + ↑d * u⁻¹) else 0

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_localization · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_layer_cube_zero (p m : ℕ) [NeZero p] [NeZero m] (hpm : p ∣ m) :

↑m ^ 3 = 0

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_layer_cube_zero · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_stationary_shift (p m : ℕ) [NeZero p] [NeZero m] (hpm : p ∣ m) (a d : ℤ) (u t : ZMod (p * (m * m))) :

IsUnit (u + ↑m * t) ∧ ↑a * (ZMod.castHom ⋯ (ZMod m)) (u + ↑m * t) ^ 2 = ↑d ↔ IsUnit u ∧ ↑a * (ZMod.castHom ⋯ (ZMod m)) u ^ 2 = ↑d

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_stationary_shift · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_stationary_linear_coefficient (p m : ℕ) [NeZero p] [NeZero m] (a d : ℤ) (u : ZMod (p * (m * m))) (hu : IsUnit u) (hs : ↑a * (ZMod.castHom ⋯ (ZMod m)) u ^ 2 = ↑d) :

∃ (c : ℕ), ↑a - ↑d * u⁻¹ ^ 2 = ↑m * ↑c

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_stationary_linear_coefficient · compiled type and proof/definition references.

source

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_stationary_phase (p m : ℕ) [NeZero p] [NeZero m] (hpm : p ∣ m) (a d : ℤ) (u t : ZMod (p * (m * m))) (hu : IsUnit u) (c : ℕ) (hc : ↑a - ↑d * u⁻¹ ^ 2 = ↑m * ↑c) :

ZMod.stdAddChar (↑a * (u + ↑m * t) + ↑d * (u + ↑m * t)⁻¹) = ZMod.stdAddChar (↑a * u + ↑d * u⁻¹) * ZMod.stdAddChar ((ZMod.castHom ⋯ (ZMod p)) (↑d * u⁻¹ ^ 3) * (ZMod.castHom ⋯ (ZMod p)) t ^ 2 + ↑c * (ZMod.castHom ⋯ (ZMod p)) t)

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.oddPrimePower_stationary_phase · compiled type and proof/definition references.