OAI/Combinatorics/ContingencyTables/Transport/FiniteIndependentAverages.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FiniteIndependentAverages.sampleSum line 16
2. def OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage line 18
3. lemma OAI.ContingencyTables.FiniteIndependentAverages.sampleSum_cons line 21
4. lemma OAI.ContingencyTables.FiniteIndependentAverages.centered_mean line 25
5. lemma OAI.ContingencyTables.FiniteIndependentAverages.sampleSum_mean_zero line 29
6. theorem OAI.ContingencyTables.FiniteIndependentAverages.sampleSum_secondMoment line 45

   Source documentation

   Mixed terms vanish because each coordinate is an independent uniform finite experiment, not because of an assumed concentration oracle.

   theorem sampleSum_secondMoment (g : X → ℝ) (hg : uniformAverage g=0) (N : ℕ) :
       uniformAverage (fun xs : Fin N → X => (sampleSum g N xs)^2)=
         N*uniformAverage (fun x => (g x)^2) := by
   …

   Mentions: OAI.ContingencyTables.FiniteIndependentAverages.sampleSum

7. lemma OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage_centered line 69
8. theorem OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage_secondMoment line 78
9. theorem OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage_failure line 87

   Source documentation

   A finite Chebyshev bound for the actual independent sample array.

   theorem sampleAverage_failure (g : X → ℝ) (N : ℕ) (hN : 0 < N)
       (sigma : ℝ) (hsigma : 0 < sigma) (hmean : 0 < uniformAverage g) :
       uniformAverage (fun xs : Fin N → X =>
         if sigma*uniformAverage g < |sampleAverage g N xs-uniformAverage g| then (1:ℝ) else 0) ≤
         uniformAverage (fun x => (g x-uniformAverage g)^2)/(N*(sigma*uniformAverage g)^2) := by
   …

   Mentions: OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage

10. lemma OAI.ContingencyTables.FiniteIndependentAverages.mean_bounds line 110
11. theorem OAI.ContingencyTables.FiniteIndependentAverages.bounded_relative_failure line 118

    Source documentation

    A bounded positive output gives the same explicit relative-variance bound on every finite experiment, including a Boolean-word sampler.

    theorem bounded_relative_failure (g : X → ℝ) (L U : ℝ) (hL : 0 < L)
        (hg : ∀ x,L ≤ g x ∧ g x ≤ U) (N : ℕ) (hN : 0 < N) (sigma : ℝ) (hsigma : 0 < sigma) :
        uniformAverage (fun xs : Fin N → X =>
          if sigma*uniformAverage g < |sampleAverage g N xs-uniformAverage g| then (1:ℝ) else 0) ≤
          U^2/(N*(sigma*L)^2) := by
    …

    Mentions: OAI.ContingencyTables.FiniteIndependentAverages.sampleAverage