OAI/Combinatorics/EditApproximation/Probability/FiniteSampling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite uniform sampling

The shared group estimator samples child labels uniformly with replacement. These lemmas use that finite distribution, including its product law; they do not assume that different group representatives are independent.

  1. def OAI.EditApproximation.uniformMean line 17
  2. theorem OAI.EditApproximation.uniform_integral line 20
  3. theorem OAI.EditApproximation.uniformMean_bounds line 28
  4. theorem OAI.EditApproximation.uniform_centered_bound line 38
  5. theorem OAI.EditApproximation.uniform_centered_integral line 44
  6. theorem OAI.EditApproximation.uniform_variance_bound line 51
  7. theorem OAI.EditApproximation.uniform_sample_average_concentration line 79

    Source documentation

    Actual independent uniform draws, centered and divided by the sample count. All measurability, centering and variance obligations for Bernstein are derived from this product distribution.

    theorem uniform_sample_average_concentration
    {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    (n : ℕ) (hn : 0 < n) (value : ι → ℝ) (bound meanBound deviation : ℝ)
    (hbound : 0 < bound) (hmeanBound : 0 < meanBound) (hdev : 0 < deviation)
    (hvalue : ∀ i, 0 ≤ value i ∧ value i ≤ bound)
    (hmean : uniformMean value ≤ meanBound)
    (bernstein : FiniteBernsteinInput
      (Measure.pi fun _ : Fin n => (PMF.uniformOfFintype ι).toMeasure)) :
    (Measure.pi fun _ : Fin n => (PMF.uniformOfFintype ι).toMeasure).real
      {ω | deviation ≤ |(∑ j : Fin n, value (ω j)) / n - uniformMean value|} ≤
      2 * Real.exp (-(n : ℝ) * deviation ^ 2 /
…

    Mentions: OAI.EditApproximation.uniformMean, OAI.EditApproximation.FiniteBernsteinInput