LocalProjection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform local projections

The finite quotient argument underlying equation valuation-tail in paper 031-01. A uniformly chosen element of a finite additive group maps uniformly to its image. A single element of large additive order in that image bounds the mass of the zero fiber. No independence between different component projections is used.

theorem OAI.DukePrimeDegree.kernel_fraction_le_inverse_order line 22

Source documentation

A single element in the image gives a bound for the proportion of the zero fiber of an additive homomorphism.

theorem kernel_fraction_le_inverse_order
    {A B : Type*} [AddGroup A] [AddGroup B] [Finite A] [Finite B]
    (f : A →+ B) (x : A) :
    (Nat.card f.ker : ℝ) / Nat.card A ≤ 1 / (addOrderOf (f x) : ℝ) := by
…

theorem OAI.DukePrimeDegree.kernel_fraction_le_prime_power line 43

Source documentation

The form used for a component modulo the kth power of its maximal ideal: a unit generates at least ℓ ^ ceil(k/e) distinct additive images.

theorem kernel_fraction_le_prime_power
    {A B : Type*} [AddGroup A] [AddGroup B] [Finite A] [Finite B]
    (f : A →+ B) (x : A) (ℓ a : ℕ) (hℓ : 0 < ℓ)
    (horder : ℓ ^ a ≤ addOrderOf (f x)) :
    (Nat.card f.ker : ℝ) / Nat.card A ≤ (ℓ : ℝ) ^ (-(a : ℤ)) := by
…