StructuredCoefficientEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The coefficient energy needed by the noncube sieve follows from the actual independent prime weights, including logarithmic weight families.

lemma OAI.CubicFirstMoment.primeMomentCoefficient_norm_le line 16
lemma OAI.CubicFirstMoment.structuredCoefficient_energy_le line 29
lemma OAI.CubicFirstMoment.LogarithmicWeightFamily.subpower_norm line 51

theorem OAI.CubicFirstMoment.logarithmic_structured_coefficient_energy line 69

Source documentation

Every specified logarithmic family has the actual subpower coefficient energy required in the nonexceptional character sieve.

theorem logarithmic_structured_coefficient_energy {L : γ → ℝ}
    {W : γ → ι → ℝ → ℂ} (hW : LogarithmicWeightFamily
      (fun z : γ × ι => L z.1) (fun z => W z.1 z.2))
    {R ε : ℝ} (hR : 0 ≤ R) (hε : 0 < ε)
    (hlo : ∀ r i x, x < 1 → W r i x = 0)
    (hhi : ∀ r i x, R < x → W r i x = 0) :
    ∃ T : ℝ, ∀ (r : γ) (X : ι → ℝ) (Z : ℝ), 1 ≤ L r → T ≤ L r →
      (∀ i, 0 < X i) → (∏ i, X i) = L r →
      (∑ z ∈ orderedConvolutionSupport (coordinatePrimeSupport (W r) X Z),
        ‖primeMomentCoefficient (W r) X Z z‖^2) ≤ (L r)^(1+ε) := by
…

Mentions: OAI.CubicFirstMoment.LogarithmicWeightFamily, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.coordinatePrimeSupport, OAI.CubicFirstMoment.primeMomentCoefficient