QuartetPairMajorant.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Mean bounds for same-pair quartet majorants

The square-fiber factor costs two for one index and costs nothing when summed over all indices. Difference convolution then multiplies masses.

def OAI.Ostmann.differenceMajorant line 20
theorem OAI.Ostmann.mean_differenceMajorant_le line 24
def OAI.Ostmann.samePairMajorant line 36
theorem OAI.Ostmann.samePairMajorant_nonneg line 41
theorem OAI.Ostmann.squareCharacterMass_normalized_sum line 48

theorem OAI.Ostmann.samePairMajorant_mean_le line 58

Source documentation

Small supremum for the same-pair majorant.

theorem samePairMajorant_mean_le {p : ℕ} [Fact p.Prime]
    (F : MulChar (ZMod p) ℂ → ZMod p → ℝ) (R : ZMod p → ℝ)
    (hF : ∀ χ d, 0 ≤ F χ d) (hR : ∀ d, 0 ≤ R d)
    (M H : ℝ) (hM : 0 ≤ M)
    (hFm : ∀ χ, (∑ d : ZMod p, F χ d) / (Fintype.card (ZMod p)ˣ : ℝ) ≤ M)
    (hRm : (∑ d : ZMod p, R d) / (Fintype.card (ZMod p)ˣ : ℝ) ≤ H)
    (ρ : MulChar (ZMod p) ℂ) :
    (∑ y : (ZMod p)ˣ, samePairMajorant F R ρ y) /
      (Fintype.card (ZMod p)ˣ : ℝ) ≤ 2 * M * H := by
…

Mentions: OAI.Ostmann.samePairMajorant

theorem OAI.Ostmann.samePairMajorant_total_mean_le line 76

Source documentation

Bounded sum over all indices for the same-pair majorant.

theorem samePairMajorant_total_mean_le {p : ℕ} [Fact p.Prime]
    (F : MulChar (ZMod p) ℂ → ZMod p → ℝ) (R : ZMod p → ℝ)
    (hF : ∀ χ d, 0 ≤ F χ d) (hR : ∀ d, 0 ≤ R d)
    (S H : ℝ) (hS : 0 ≤ S)
    (hFs : (∑ χ : MulChar (ZMod p) ℂ,
      (∑ d : ZMod p, F χ d) / (Fintype.card (ZMod p)ˣ : ℝ)) ≤ S)
    (hRm : (∑ d : ZMod p, R d) / (Fintype.card (ZMod p)ˣ : ℝ) ≤ H) :
    (∑ ρ : MulChar (ZMod p) ℂ, (∑ y : (ZMod p)ˣ, samePairMajorant F R ρ y) /
      (Fintype.card (ZMod p)ˣ : ℝ)) ≤ S * H := by
…

Mentions: OAI.Ostmann.samePairMajorant