Binomial.lean`

162 declarations, 0 contain sorry, 0 declared as axioms

Binomial

Fair and biased binomial laws, generating series, differences, concentration, Gaussian overlap, hidden counts, and local lower bounds.

def OAI.TraceReconstruction.fairBinomial line 24
Source documentation
Fair-binomial mass, extended by zero beyond its natural support.
```
def fairBinomial (n k : ℕ) : ℝ := (n.choose k : ℝ) / 2 ^ n
```
theorem OAI.TraceReconstruction.fairBinomial_nonneg line 26
theorem OAI.TraceReconstruction.centralBinom_square_bound line 30
theorem OAI.TraceReconstruction.choose_odd_le_twice_central line 59
theorem OAI.TraceReconstruction.fairBinomial_square_bound line 69
abbrev OAI.TraceReconstruction.IntSeries line 108
def OAI.TraceReconstruction.seriesL1 line 110
def OAI.TraceReconstruction.seriesL2Sq line 111
theorem OAI.TraceReconstruction.series_summable line 113
theorem OAI.TraceReconstruction.seriesL1_nonneg line 117
theorem OAI.TraceReconstruction.seriesL2Sq_nonneg line 120
theorem OAI.TraceReconstruction.seriesL1_eq_sum line 123
theorem OAI.TraceReconstruction.seriesL2Sq_eq_sum line 129
theorem OAI.TraceReconstruction.series_summable_shift line 135
theorem OAI.TraceReconstruction.series_sum_shift line 140
theorem OAI.TraceReconstruction.series_coeff_mul_abs_le line 144
theorem OAI.TraceReconstruction.seriesL1_mul_le line 150
theorem OAI.TraceReconstruction.series_coeff_mul_sq_le line 166
theorem OAI.TraceReconstruction.seriesL2Sq_mul_le line 176
theorem OAI.TraceReconstruction.series_coeff_mul_bound line 195
def OAI.TraceReconstruction.fairSeries line 206
theorem OAI.TraceReconstruction.fairSeries_add line 209
theorem OAI.TraceReconstruction.fairSeries_sum line 212
theorem OAI.TraceReconstruction.fairSeries_coeff_nat line 230
theorem OAI.TraceReconstruction.fairSeries_coeff_neg line 246
theorem OAI.TraceReconstruction.seriesL1_eq_sum_range line 254
def OAI.TraceReconstruction.firstDifference line 273
theorem OAI.TraceReconstruction.firstDifference_coeff line 276
theorem OAI.TraceReconstruction.fairSeries_difference_coeff_zero line 283
theorem OAI.TraceReconstruction.fairSeries_difference_coeff_succ line 290
theorem OAI.TraceReconstruction.fairBinomial_unimodal_left line 296
theorem OAI.TraceReconstruction.fairBinomial_unimodal_right line 301
theorem OAI.TraceReconstruction.fairBinomial_variation line 309
theorem OAI.TraceReconstruction.fairSeries_difference_L1 line 338
def OAI.TraceReconstruction.binomialBound line 356
theorem OAI.TraceReconstruction.binomialBound_nonneg line 358
theorem OAI.TraceReconstruction.fairBinomial_le_bound line 360
theorem OAI.TraceReconstruction.fairSeries_nonneg line 365
theorem OAI.TraceReconstruction.fairSeries_coeff_bound line 371
theorem OAI.TraceReconstruction.fairSeries_L1 line 380
theorem OAI.TraceReconstruction.seriesL2Sq_le_L1_mul_bound line 392
theorem OAI.TraceReconstruction.fairSeries_L2Sq_bound line 405
theorem OAI.TraceReconstruction.fairSeries_difference_L1_bound line 409
theorem OAI.TraceReconstruction.seriesL1_single line 414
theorem OAI.TraceReconstruction.seriesL1_one line 421
theorem OAI.TraceReconstruction.seriesL1_pow_le line 425
theorem OAI.TraceReconstruction.fairSeries_mul_power line 433
theorem OAI.TraceReconstruction.binomial_difference_coeff_bound line 441
Source documentation
Quantitative higher-order smoothing, with n trials assigned to each difference and one further group reserved for anti-concentration.
```
theorem binomial_difference_coeff_bound (n s : ℕ) (z : ℤ) :
    |(firstDifference ^ s * fairSeries ((s + 1) * n)).coeff z| ≤
      (2 * binomialBound n) ^ s * binomialBound n := by
…
```
Mentions: OAI.TraceReconstruction.firstDifference, OAI.TraceReconstruction.fairSeries, OAI.TraceReconstruction.binomialBound
theorem OAI.TraceReconstruction.binomial_difference_L2Sq_bound line 450
theorem OAI.TraceReconstruction.seriesL1_add_le line 463
theorem OAI.TraceReconstruction.seriesL1_zero line 475
theorem OAI.TraceReconstruction.seriesL1_sum_le line 478
theorem OAI.TraceReconstruction.seriesL1_prod_le line 487
def OAI.TraceReconstruction.geomSeries line 496
def OAI.TraceReconstruction.prouhetSeries line 498
def OAI.TraceReconstruction.prouhetQuotient line 501
theorem OAI.TraceReconstruction.geomSeries_difference line 504
theorem OAI.TraceReconstruction.geomSeries_L1_le line 508
theorem OAI.TraceReconstruction.prouhetSeries_factor line 513
theorem OAI.TraceReconstruction.prouhetQuotient_L1_le line 520
theorem OAI.TraceReconstruction.prouhet_binomial_coeff_bound line 538
Source documentation
Prouhet smoothing in an explicit finite-trial form. The constants 2^(s*s) and (2 sqrt(2/(n+1)))^s are exp(O(s^2)) after assigning n = floor(g/(s+1)) trials to each group. No Fourier theorem or probabilistic estimate is assumed.
```
theorem prouhet_binomial_coeff_bound (n s : ℕ) (z : ℤ) :
    |(prouhetSeries s * fairSeries ((s + 1) * n)).coeff z| ≤
      (2 : ℝ) ^ (s * s) * ((2 * binomialBound n) ^ s * binomialBound n) := by
…
```
Mentions: OAI.TraceReconstruction.prouhetSeries, OAI.TraceReconstruction.fairSeries, OAI.TraceReconstruction.binomialBound
theorem OAI.TraceReconstruction.prouhet_binomial_L2Sq_bound line 546
theorem OAI.TraceReconstruction.prouhet_binomial_coeff_bound_remainder line 559
Source documentation
Arbitrary trial counts are obtained by convolving with the independent unused trials; this cannot enlarge the coefficient or squared-L2 bounds.
```
theorem prouhet_binomial_coeff_bound_remainder (n s r : ℕ) (z : ℤ) :
    |(prouhetSeries s * fairSeries ((s + 1) * n + r)).coeff z| ≤
      (2 : ℝ) ^ (s * s) * ((2 * binomialBound n) ^ s * binomialBound n) := by
…
```
Mentions: OAI.TraceReconstruction.prouhetSeries, OAI.TraceReconstruction.fairSeries, OAI.TraceReconstruction.binomialBound
theorem OAI.TraceReconstruction.prouhet_binomial_L2Sq_bound_remainder line 567
theorem OAI.TraceReconstruction.signed_binomial_smoothing line 577
theorem OAI.TraceReconstruction.binomialBound_quotient_le line 592
theorem OAI.TraceReconstruction.prouhetSeries_succ_coeff line 606
theorem OAI.TraceReconstruction.prouhetSeries_coeff_spec line 618
Source documentation
The exact generating polynomial from the manuscript has unit signed coefficients at every index 0,...,2^s-1, and no other coefficients.
```
theorem prouhetSeries_coeff_spec (s : ℕ) :
    (∀ z : ℤ, (z < 0 ∨ (2 ^ s : ℕ) ≤ z) → (prouhetSeries s).coeff z = 0) ∧
    (∀ z : ℤ, 0 ≤ z → z < (2 ^ s : ℕ) → |(prouhetSeries s).coeff z| = 1) := by
…
```
Mentions: OAI.TraceReconstruction.prouhetSeries
def OAI.TraceReconstruction.binomialMass line 657
theorem OAI.TraceReconstruction.binomialMass_nonneg line 660
theorem OAI.TraceReconstruction.sum_binomialMass line 665
theorem OAI.TraceReconstruction.binomialMass_harmonic_step line 675
theorem OAI.TraceReconstruction.binomialMass_harmonic_identity line 686
theorem OAI.TraceReconstruction.binomialMass_harmonic_le line 698

theorem OAI.TraceReconstruction.weighted_sum_sq_le line 707

Source documentation

The weighted Cauchy--Schwarz step for mixing the fair estimates.

theorem weighted_sum_sq_le {ι : Type*} (S : Finset ι) (w f : ι → ℝ)
    (hw : ∀ i, 0 ≤ w i) :
    (∑ i ∈ S, w i * f i) ^ 2 ≤ (∑ i ∈ S, w i) * ∑ i ∈ S, w i * f i ^ 2 := by
…

theorem OAI.TraceReconstruction.mixed_binomialBound_le line 717
def OAI.TraceReconstruction.mixedFairSeries line 747
def OAI.TraceReconstruction.biasedSeries line 750
theorem OAI.TraceReconstruction.mixedFairSeries_expansion line 753
theorem OAI.TraceReconstruction.mixedFairSeries_eq_biased line 765
theorem OAI.TraceReconstruction.mixedFairSeries_coeff_bound line 775
theorem OAI.TraceReconstruction.biasedSeries_coeff_bound_low line 792
Source documentation
At success probabilities at most 1/2, this gives the sharp variance scale up to an absolute constant, using only the fair-coin estimate.
```
theorem biasedSeries_coeff_bound_low (n : ℕ) {p : ℝ}
    (hp : p ∈ Set.Ioc 0 (1 / 2)) (z : ℤ) :
    |(biasedSeries n p).coeff z| ≤ Real.sqrt (1 / (((n : ℝ) + 1) * p)) := by
…
```
Mentions: OAI.TraceReconstruction.biasedSeries
theorem OAI.TraceReconstruction.biasedSeries_sum line 803
theorem OAI.TraceReconstruction.biasedSeries_coeff_nat line 817
theorem OAI.TraceReconstruction.biasedSeries_coeff_neg line 833
theorem OAI.TraceReconstruction.biasedSeries_coeff_high line 841
theorem OAI.TraceReconstruction.binomialMass_symm line 849
theorem OAI.TraceReconstruction.biasedSeries_coeff_reflect line 855
theorem OAI.TraceReconstruction.biasedSeries_coeff_bound line 872
Source documentation
Uniform nonfair-binomial anti-concentration. This is the absolute variance-scale upper bound used in the manuscript's rank kernels.
```
theorem biasedSeries_coeff_bound (n : ℕ) {p : ℝ}
    (hp : p ∈ Set.Ioo 0 1) (z : ℤ) :
    |(biasedSeries n p).coeff z| ≤
      Real.sqrt (1 / (((n : ℝ) + 1) * p * (1 - p))) := by
…
```
Mentions: OAI.TraceReconstruction.biasedSeries
theorem OAI.TraceReconstruction.binomialMass_mul_index line 893
theorem OAI.TraceReconstruction.binomialMass_index_sum line 901
theorem OAI.TraceReconstruction.binomialMass_mean line 913
theorem OAI.TraceReconstruction.binomialMass_second_moment line 921
theorem OAI.TraceReconstruction.binomialMass_variance line 938
theorem OAI.TraceReconstruction.binomialMass_adjacent line 951
theorem OAI.TraceReconstruction.binomialMass_le_mode line 963

theorem OAI.TraceReconstruction.discrete_mode_lower line 1005

Source documentation

A discrete law cannot have a very small maximum when its variance is bounded. The explicit constant is deliberately loose, avoiding any use of Stirling.

theorem discrete_mode_lower (n l : ℕ) (f : ℕ → ℝ) (M v : ℝ)
    (hf : ∀ k, 0 ≤ f k) (hsum : ∑ k ∈ Finset.range (n + 1), f k = 1)
    (hmax : ∀ k, f k ≤ M)
    (hvar : ∑ k ∈ Finset.range (n + 1), f k * ((k : ℝ) - l) ^ 2 = v)
    (hv : 1 ≤ v) : 1 / (12 * Real.sqrt v) ≤ M := by
…

theorem OAI.TraceReconstruction.binomialMass_mean_lower line 1062
theorem OAI.TraceReconstruction.binomialMass_mean_inverse_sq line 1074
theorem OAI.TraceReconstruction.seriesL1_smul line 1090
theorem OAI.TraceReconstruction.mixedFairSeries_difference_L1_bound line 1096
theorem OAI.TraceReconstruction.biasedSeries_difference_L1_bound_low line 1116
theorem OAI.TraceReconstruction.biasedSeries_difference_reflect line 1130
theorem OAI.TraceReconstruction.biasedSeries_difference_L1_reflect line 1146
theorem OAI.TraceReconstruction.biasedSeries_difference_L1_bound line 1154
def OAI.TraceReconstruction.biasedBinomialBound line 1175
theorem OAI.TraceReconstruction.biasedSeries_L1 line 1178
theorem OAI.TraceReconstruction.biasedSeries_L2Sq_bound line 1186
theorem OAI.TraceReconstruction.biasedSeries_add line 1191
theorem OAI.TraceReconstruction.biasedSeries_mul_power line 1195
theorem OAI.TraceReconstruction.biased_difference_coeff_bound line 1201
theorem OAI.TraceReconstruction.biased_difference_L2Sq_bound line 1210
theorem OAI.TraceReconstruction.biased_difference_coeff_bound_remainder line 1223
theorem OAI.TraceReconstruction.biased_difference_L2Sq_bound_remainder line 1232

theorem OAI.TraceReconstruction.biased_difference_smoothing line 1245

Source documentation

All fixed-order nonfair binomial differences, at the exact variance scale. This is the analytic estimate needed for the initial conditional rank kernels.

theorem biased_difference_smoothing (g s : ℕ) {p : ℝ} (hp : p ∈ Set.Ioo 0 1) :
    (∀ z : ℤ, |(firstDifference ^ s * biasedSeries g p).coeff z| ≤
      (2 * biasedBinomialBound (g / (s + 1)) p) ^ s *
        biasedBinomialBound (g / (s + 1)) p) ∧
    (seriesL2Sq (firstDifference ^ s * biasedSeries g p) ≤
      ((2 * biasedBinomialBound (g / (s + 1)) p) ^ s) ^ 2 *
        biasedBinomialBound (g / (s + 1)) p) := by
…

Mentions: OAI.TraceReconstruction.firstDifference, OAI.TraceReconstruction.biasedSeries, OAI.TraceReconstruction.biasedBinomialBound, OAI.TraceReconstruction.seriesL2Sq

theorem OAI.TraceReconstruction.biasedBinomialBound_quotient_le line 1260
theorem OAI.TraceReconstruction.binomialMass_tilt line 1282
theorem OAI.TraceReconstruction.binomialMass_tilt_product line 1299

theorem OAI.TraceReconstruction.binomial_overlap_tilt_bound line 1316

Source documentation

Tilting on opposite sides retains an anti-concentration factor as well as the Gaussian penalty for different numbers of trials.

theorem binomial_overlap_tilt_bound (g h : ℕ) {p a : ℝ}
    (hp : p ∈ Set.Ioo 0 1) (ha : 0 < a) :
    (∑ k ∈ Finset.range (h + 1), binomialMass g p k * binomialMass h p k) ≤
      ((1 - p + p * a) ^ g * (1 - p + p / a) ^ h) *
        biasedBinomialBound g (p * a / (1 - p + p * a)) := by
…

Mentions: OAI.TraceReconstruction.binomialMass, OAI.TraceReconstruction.biasedBinomialBound

theorem OAI.TraceReconstruction.binomial_tilt_variance line 1346
theorem OAI.TraceReconstruction.binomial_tilt_normalizer line 1366

theorem OAI.TraceReconstruction.binomial_gaussian_overlap line 1424

Source documentation

The Gaussian cross-overlap estimate used by the conditional rank-kernel square-sum argument. The constant is absolute, also as p tends to one.

theorem binomial_gaussian_overlap (g h : ℕ) {p : ℝ}
    (hp : p ∈ Set.Ico (1 / 2 : ℝ) 1) (hhg : h ≤ g) (hS : 0 < g + h) :
    (∑ k ∈ Finset.range (h + 1), binomialMass g p k * binomialMass h p k) ≤
      Real.sqrt (2 / (((g : ℝ) + 1) * p * (1 - p))) *
        Real.exp (-((g : ℝ) - h) ^ 2 / (16 * ((g : ℝ) + h))) := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.sqrt_times_gaussian_le line 1460
theorem OAI.TraceReconstruction.sqrt_recip_product_le line 1472
theorem OAI.TraceReconstruction.binomialMass_le_bound line 1481
theorem OAI.TraceReconstruction.binomial_product_sup line 1489
Source documentation
A uniform product-supremum estimate, including very unequal trial counts. This justifies eliminating a largest gap in the rank kernel.
```
theorem binomial_product_sup (g h k : ℕ) {p : ℝ}
    (hp : p ∈ Set.Ico (1 / 2 : ℝ) 1) :
    binomialMass g p k * binomialMass h p k ≤
      32 / (((g : ℝ) + 1) * p * (1 - p)) := by
…
```
Mentions: OAI.TraceReconstruction.binomialMass
theorem OAI.TraceReconstruction.binomialMass_mgf line 1553
Source documentation
Exact moment generating function, including both endpoint channels.
```
theorem binomialMass_mgf (n : ℕ) (p t : ℝ) :
    (∑ k ∈ Finset.range (n + 1), binomialMass n p k * Real.exp (t * k)) =
      (1 - p + p * Real.exp t) ^ n := by
…
```
Mentions: OAI.TraceReconstruction.binomialMass
theorem OAI.TraceReconstruction.binomialMass_mgf_le line 1563

theorem OAI.TraceReconstruction.finite_exp_markov line 1575

Source documentation

Exponential Markov bound for a finite nonnegative measure.

theorem finite_exp_markov {α : Type*} (S : Finset α) (w X : α → ℝ)
    (hw : ∀ a ∈ S, 0 ≤ w a) (a t : ℝ) (ht : 0 ≤ t) :
    (∑ z ∈ S with a ≤ X z, w z) ≤
      Real.exp (-t * a) * ∑ z ∈ S, w z * Real.exp (t * X z) := by
…

theorem OAI.TraceReconstruction.binomialMass_lower_half line 1600

Source documentation

A uniform multiplicative lower tail, sufficient for hidden-flag counts.

theorem binomialMass_lower_half (n : ℕ) {p : ℝ} (hp : p ∈ Set.Icc 0 1) :
    (∑ k ∈ (Finset.range (n + 1)).filter (fun k : ℕ => (k : ℝ) ≤ n * p / 2),
      binomialMass n p k) ≤ Real.exp (-(n : ℝ) * p / 12) := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.fairBinomial_centered_mgf line 1639
theorem OAI.TraceReconstruction.fairBinomial_upper_tail line 1666
def OAI.TraceReconstruction.hypergeomMass line 1688
theorem OAI.TraceReconstruction.hypergeomMass_nonneg line 1691
theorem OAI.TraceReconstruction.hypergeomMass_eq_binomial line 1695
theorem OAI.TraceReconstruction.binomialMass_sq_upper line 1722
theorem OAI.TraceReconstruction.hypergeomMass_sq_upper line 1732
theorem OAI.TraceReconstruction.sum_hypergeomMass line 1756
theorem OAI.TraceReconstruction.hypergeomMass_high line 1774
theorem OAI.TraceReconstruction.hypergeom_hidden_adjacent line 1781
Source documentation
Adjacent-mass identity for the hidden count. The central regime has full support on 0,...,M; this is exactly the regime used in adjacent-power lifting.
```
theorem hypergeom_hidden_adjacent (V M m k : ℕ) (hM : M ≤ m) (hV : m ≤ V) (hk : k < M) :
    (((k:ℝ)+1)*((V:ℝ)-m+k+1)) * hypergeomMass M V m (k+1) =
    (((M:ℝ)-k)*((m:ℝ)-k)) * hypergeomMass M V m k := by
…
```
Mentions: OAI.TraceReconstruction.hypergeomMass
def OAI.TraceReconstruction.hypergeomHiddenMode line 1808
theorem OAI.TraceReconstruction.hypergeomHiddenMode_le line 1810
theorem OAI.TraceReconstruction.hypergeom_hidden_unimodal_left line 1819
theorem OAI.TraceReconstruction.hypergeom_hidden_unimodal_right line 1835

theorem OAI.TraceReconstruction.unimodal_variation line 1853

Source documentation

Exact total variation of a zero-extended unimodal sequence.

theorem unimodal_variation (f : ℕ → ℝ) (n l : ℕ) (hl : l ≤ n+1)
    (hleft : ∀ k < l, f k ≤ f (k+1))
    (hright : ∀ k, l ≤ k → f (k+1) ≤ f k) (hz : f (n+1)=0) :
    f 0 + ∑ k ∈ Finset.range (n+1), |f (k+1)-f k| = 2*f l := by
…

theorem OAI.TraceReconstruction.hypergeom_hidden_variation line 1873
theorem OAI.TraceReconstruction.choose_pred_weight line 1882
theorem OAI.TraceReconstruction.choose_pred_weight_succ line 1890
def OAI.TraceReconstruction.hypergeomHiddenFlux line 1896
theorem OAI.TraceReconstruction.hypergeomHiddenFlux_formula line 1899
theorem OAI.TraceReconstruction.hypergeomHiddenFlux_high line 1927
theorem OAI.TraceReconstruction.hypergeomHiddenFlux_boundary line 1931
theorem OAI.TraceReconstruction.hypergeom_adjacent_hidden_difference line 1940
theorem OAI.TraceReconstruction.hypergeom_next_zero line 1995
def OAI.TraceReconstruction.adjacentHypergeomTV line 2015
Source documentation
Exact adjacent visible-count TV, expressed with complementary hidden counts. The shift by one is essential: the two totals are different.
```
def adjacentHypergeomTV (V M m : ℕ) : ℝ :=
…
```
theorem OAI.TraceReconstruction.adjacentHypergeomTV_eq_flux line 2019
theorem OAI.TraceReconstruction.adjacentHypergeomTV_le_mass line 2036
def OAI.TraceReconstruction.bernoulliRelativeEntropy line 2051
theorem OAI.TraceReconstruction.bernoulliRelativeEntropy_upper line 2054
theorem OAI.TraceReconstruction.binomialMass_change_probability line 2066
theorem OAI.TraceReconstruction.binomialMass_mean_change_probability line 2077

theorem OAI.TraceReconstruction.binomialMass_local_lower line 2091

Source documentation

Uniform local binomial lower bound without Stirling. It applies at a count k by changing to the channel with mean exactly k.

theorem binomialMass_local_lower (n k : ℕ) {θ p : ℝ}
    (hθ : θ ∈ Set.Ioo 0 1) (hp : p ∈ Set.Ioo 0 1)
    (hk : k ≤ n) (hmean : (n:ℝ)*θ = k) (hv : 1 ≤ (n:ℝ)*θ*(1-θ)) :
    Real.exp (-(n:ℝ)*(θ-p)^2/(p*(1-p))) /
      (12*Real.sqrt ((n:ℝ)*θ*(1-θ))) ≤ binomialMass n p k := by
…

Mentions: OAI.TraceReconstruction.binomialMass