Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistBoundedError

Two-sided Frobenius-twist errors from the bounded average #

The exact average of the infinity-place contributions is not needed to obtain a two-sided estimate for an individual Frobenius twist. The already-proved bounded aggregate error, together with a common one-sided Stepanov bound for all twists, suffices by finite averaging.

This is the direct function-field specialization of abs_le_of_uniform_upper_and_abs_sum_le.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.boundedErrorBaseConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] :
Algebra C N

The algebra structure from C to N used in the exact constant extension frobenius twist bounded error construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.boundedErrorBaseConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] :
    IsScalarTower C (RatFunc C) N
    source
    theorem BGS.HasseWeil.abs_frobeniusTwistFieldRationalPlaceError_le_of_uniform_upper (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) (g : Gal(N/RatFunc C)) (B : ℝ) (hB : 0 ≤ B) (hupper : ∀ (τ : Gal(N/RatFunc C)), ↑(frobeniusTwistFieldRationalPlaceCount C S N hExact τ) - ↑(Nat.card C) - 1 ≤ B) :
    |↑(frobeniusTwistFieldRationalPlaceCount C S N hExact g) - ↑(Nat.card C) - 1| ≤ ↑(Nat.card Gal(N/RatFunc C)) * ↑(Module.finrank (RatFunc C) N) + ↑(Nat.card Gal(N/RatFunc C) - 1) * B

    A common upper bound for all Frobenius-twist point-count errors gives a two-sided bound for every twist. The additive term is uniform in the auxiliary constant extension S: it depends only on the original Galois group and the degree of N / C(X).

    Consequently, the exact infinity-place average is not a prerequisite for the two-sided estimate used in a Hasse--Weil argument.