OAI/NumberTheory/TwoPoint/Bounds/TriangleKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A direct finite-law small-ball inequality using a nonnegative triangular Fourier kernel. This replaces any need for an external concentration theorem.

  1. def OAI.TwoPointCorrelations.triangleKernel line 15
  2. lemma OAI.TwoPointCorrelations.triangleKernel_zero line 18
  3. lemma OAI.TwoPointCorrelations.triangleKernel_eq line 25
  4. lemma OAI.TwoPointCorrelations.triangleKernel_nonneg line 44
  5. lemma OAI.TwoPointCorrelations.triangleKernel_unit_lower line 50
  6. lemma OAI.TwoPointCorrelations.FiniteLaw.average_triangleKernel line 74
  7. theorem OAI.TwoPointCorrelations.FiniteLaw.unit_small_ball_le line 99

    Source documentation

    The exact finite-law small-ball reduction. The characteristic function can now be bounded inside a compact ordinary integral.

    theorem FiniteLaw.unit_small_ball_le {Ω : Type*} [Fintype Ω]
    (μ : FiniteLaw Ω) (Z : Ω → ℝ) :
    μ.probability (fun x => |Z x| ≤ 1) ≤
      4 * (∫ t in (0 : ℝ)..1, (1 - t) * μ.average (fun x => Real.cos (t * Z x))) := by
…

    Mentions: OAI.TwoPointCorrelations.FiniteLaw