JointSquareLiftExclusions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Dropping all prime-square exclusions in the uniform CRT fibers

theorem OAI.Ostmann.squareLiftPairs_card line 12
theorem OAI.Ostmann.squareLiftPairs_nonempty line 16

theorem OAI.Ostmann.joint_square_lift_removed_mass_le line 22

Source documentation

A simultaneous lift comparison for a signed integrand. The remaining arithmetic conditions can be included in F; they are never conditioned away.

theorem joint_square_lift_removed_mass_le {I : Type*} [Fintype I] [DecidableEq I]
    (p : I → ℕ) [∀ i, Fact (p i).Prime] (J : I → Type*) [∀ i, Fintype (J i)]
    (a b : ∀ i, J i → ZMod (p i ^ 2)) (x₀ y₀ : ∀ i, ZMod (p i))
    (hy : ∀ i, y₀ i ≠ 0)
    (hrow : ∀ i j, squareReduction (p i) (a i j) ≠ 0 ∨ squareReduction (p i) (b i j) ≠ 0)
    (hbase : ∀ i j, squareReduction (p i) (a i j) * x₀ i +
      squareReduction (p i) (b i j) * y₀ i = 0)
    (F : (∀ i, SquareLiftPairs (p i) (x₀ i) (y₀ i)) → ℂ)
    (B : ℝ) (hB : 0 ≤ B) (hF : ∀ x, ‖F x‖ ≤ B) :
    (Fintype.card (∀ i, SquareLiftPairs (p i) (x₀ i) (y₀ i)) : ℝ)⁻¹ *
      ‖(∑ x, if ∀ i j, a i j * (x i).1.1 + b i j * (x i).2.1 ≠ 0 then F x else 0) -
        ∑ x, F x‖ ≤ 2 * B * ∑ i, (Fintype.card (J i) : ℝ) / p i := by
…

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