OAI/NumberTheory/Ostmann/Arithmetic/SquareLiftExclusions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.SquareLiftPairs line 13

   Source documentation

   Uniform pairs over the fixed giant residues modulo p.

   abbrev SquareLiftPairs (p : ℕ) (x₀ y₀ : ZMod p) :=
   …

2. def OAI.Ostmann.zeroLiftEquiv line 17
3. theorem OAI.Ostmann.card_zeroLift line 28
4. def OAI.Ostmann.squareLiftBad line 38

   Source documentation

   All forbidden prime-square zeros, one for each occurrence of the prime.

   noncomputable def squareLiftBad {I : Type*} [Fintype I] {p : ℕ} [Fact p.Prime]
       (a : I → (ZMod (p ^ 2))ˣ) (b : I → ZMod (p ^ 2)) (x₀ y₀ : ZMod p) :
       Finset (SquareLiftPairs p x₀ y₀) := by
   …

   Mentions: OAI.Ostmann.SquareLiftPairs

5. theorem OAI.Ostmann.card_squareLiftBad_le line 44
6. theorem OAI.Ostmann.square_lift_removed_mass_le line 63

   Source documentation

   A bounded integrand loses at most B * (# occurrences) / p when all prime-square exclusions are imposed. No independence of the exclusions is used.

   theorem square_lift_removed_mass_le {I : Type*} [Fintype I] {p : ℕ} [Fact p.Prime]
       (a : I → (ZMod (p ^ 2))ˣ) (b : I → ZMod (p ^ 2)) (x₀ y₀ : ZMod p)
       (hbase : ∀ i, squareReduction p (a i) * x₀ + squareReduction p (b i) * y₀ = 0)
       (F : SquareLiftPairs p x₀ y₀ → ℂ) (B : ℝ) (hB : 0 ≤ B)
       (hF : ∀ v, ‖F v‖ ≤ B) :
       ‖∑ v ∈ squareLiftBad a b x₀ y₀, F v‖ / (p : ℝ) ^ 2 ≤
         B * (Fintype.card I : ℝ) / p := by
   …

   Mentions: OAI.Ostmann.squareReduction, OAI.Ostmann.SquareLiftPairs, OAI.Ostmann.squareLiftBad

7. theorem OAI.Ostmann.square_lift_nonzero_rows_removed_mass_le line 88

   Source documentation

   The form used in both giant environments: the second giant has a nonzero residue, and every occurrence has a nonzero row. This supplies the unit coefficient needed for the lift count rather than assuming it separately.

   theorem square_lift_nonzero_rows_removed_mass_le {I : Type*} [Fintype I]
       {p : ℕ} [Fact p.Prime] (a b : I → ZMod (p ^ 2)) (x₀ y₀ : ZMod p)
       (hy : y₀ ≠ 0)
       (hrow : ∀ i, squareReduction p (a i) ≠ 0 ∨ squareReduction p (b i) ≠ 0)
       (hbase : ∀ i, squareReduction p (a i) * x₀ + squareReduction p (b i) * y₀ = 0)
       (F : SquareLiftPairs p x₀ y₀ → ℂ) (B : ℝ) (hB : 0 ≤ B)
       (hF : ∀ v, ‖F v‖ ≤ B) :
       ‖∑ v ∈ Finset.univ.filter (fun v : SquareLiftPairs p x₀ y₀ =>
         ∃ i, a i * v.1.1 + b i * v.2.1 = 0), F v‖ / (p : ℝ) ^ 2 ≤
         B * (Fintype.card I : ℝ) / p := by
   …

   Mentions: OAI.Ostmann.squareReduction, OAI.Ostmann.SquareLiftPairs