OAI/NumberTheory/TwoPoint/Bounds/SampleDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact densities on the Boolean cube induced by a finite sampling map.

  1. def OAI.TwoPointCorrelations.sampleDensity line 13

    Source documentation

    Density relative to uniform measure of a finite uniformly sampled map.

    noncomputable def sampleDensity {α : Type*} [Fintype α] {n : ℕ}
    (sample : α → BooleanCube n) (x : BooleanCube n) : ℝ :=
…

    Mentions: OAI.TwoPointCorrelations.BooleanCube

  2. lemma OAI.TwoPointCorrelations.sampleDensity_nonneg line 18
  3. lemma OAI.TwoPointCorrelations.sampleDensity_expectation line 24

    Source documentation

    Expectations against the induced density are exactly empirical averages.

    lemma sampleDensity_expectation {α : Type*} [Fintype α] [Nonempty α] {n : ℕ}
    (sample : α → BooleanCube n) (F : BooleanCube n → ℝ) :
    cubeAverage (fun x => sampleDensity sample x * F x) =
      uniformAverage (fun a => F (sample a)) := by
…

    Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.cubeAverage, OAI.TwoPointCorrelations.sampleDensity, OAI.TwoPointCorrelations.uniformAverage

  4. lemma OAI.TwoPointCorrelations.sampleDensity_mean line 50
  5. lemma OAI.TwoPointCorrelations.sampleDensity_walshCoefficient line 54