DeficiencyVariance.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Deficiency under sampling without replacement

The variance estimate in the paper's deficiency lemma is a specialization of the finite completion-coupling theorem Balanced.WithoutReplacement.finiteVariance_powersetCard_le. Its probability space is exactly the uniform law on all size-v subsets of the supplied domain U, including the cases v = 0 and v = |U|.

def OAI.LowSpaceSubsetSum.meanDeficiency line 24
Source documentation
Mean deficiency of a uniform size-v subset of U.
```
noncomputable def meanDeficiency (a : ι → ℤ) (U : Finset ι) (v : ℕ) : ℝ :=
…
```
def OAI.LowSpaceSubsetSum.deficiencyVariance line 28
Source documentation
Variance for uniform sampling of exactly v indices, without replacement.
```
noncomputable def deficiencyVariance (a : ι → ℤ) (U : Finset ι) (v : ℕ) : ℝ :=
…
```
theorem OAI.LowSpaceSubsetSum.deficiency_exchange_bound line 31
theorem OAI.LowSpaceSubsetSum.deficiencyVariance_le line 39
Source documentation
The paper's exact variance bound Var(d(V)) ≤ v.
```
theorem deficiencyVariance_le (a : ι → ℤ) (U : Finset ι) (v : ℕ)
    (hv : v ≤ U.card) : deficiencyVariance a U v ≤ v := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiencyVariance
theorem OAI.LowSpaceSubsetSum.deficiency_centered_secondMoment_le line 47
theorem OAI.LowSpaceSubsetSum.deficiency_tail_fraction_le line 54
Source documentation
A direct finite Chebyshev bound for deviations from the mean deficiency. The left side is the exact probability under uniform size-v sampling.
```
theorem deficiency_tail_fraction_le (a : ι → ℤ) (U : Finset ι) (v : ℕ)
    (hv : v ≤ U.card) {t : ℝ} (ht : 0 < t) :
    (((U.powersetCard v).filter
      (fun V => t ≤ |deficiency a V - meanDeficiency a U v|)).card : ℝ) /
        (U.powersetCard v).card ≤ (v : ℝ) / t ^ 2 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.deficiency, OAI.LowSpaceSubsetSum.meanDeficiency

theorem OAI.LowSpaceSubsetSum.deficiency_uniform_variance_le line 89

Source documentation

Measure-theoretic form for the actual uniform fixed-cardinality law.

theorem deficiency_uniform_variance_le
    [MeasurableSpace (Finset ι)] [MeasurableSingletonClass (Finset ι)]
    (a : ι → ℤ) (U : Finset ι) (v : ℕ) (hv : v ≤ U.card) :
    ProbabilityTheory.variance (deficiency a)
      (PMF.uniformOfFinset (U.powersetCard v)
        (Finset.powersetCard_nonempty.mpr hv)).toMeasure ≤ v := by
…

Mentions: OAI.LowSpaceSubsetSum.deficiency