BernoulliComparison.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Mutually exclusive site hits versus independent Bernoulli hits

At one prime the actual site hits are mutually exclusive. Their categorical law differs from independent Bernoulli hits by at most twice the square of the sum of the site probabilities in L¹. Everything here is a finite-sum proof; no coupling estimate is assumed.

def OAI.JointDickman.categoricalSubsetMass line 20
Source documentation
Empty hit set with mass 1-sum q, singleton {i} with mass q i, and zero on every other subset. The delta-sum form avoids any choices.
```
noncomputable def categoricalSubsetMass {α : Type*} [DecidableEq α]
    (P : Finset α) (q : α → ℝ) (S : Finset α) : ℝ :=
…
```
theorem OAI.JointDickman.sum_singleton_kernel line 25
theorem OAI.JointDickman.categoricalSubsetMass_empty line 34
theorem OAI.JointDickman.categoricalSubsetMass_singleton line 39
theorem OAI.JointDickman.categoricalSubsetMass_sum line 45
theorem OAI.JointDickman.categoricalSubsetMass_nonneg line 53
theorem OAI.JointDickman.complement_product_lower line 61
theorem OAI.JointDickman.bernoulli_singleton_le line 75
theorem OAI.JointDickman.singleton_deficit_le line 86

theorem OAI.JointDickman.categorical_bernoulli_l1_eq line 103

Source documentation

An exact identity: twice the total singleton deficit is the entire L¹ discrepancy. The empty-set excess and multi-hit mass balance it.

theorem categorical_bernoulli_l1_eq {α : Type*} [DecidableEq α]
    (P : Finset α) (q : α → ℝ) (hq : ∀ i ∈ P, 0 ≤ q i ∧ q i ≤ 1) :
    (∑ S ∈ P.powerset, |categoricalSubsetMass P q S - bernoulliSubsetMass P q S|) =
      2 * ∑ i ∈ P, (q i - bernoulliSubsetMass P q {i}) := by
…

Mentions: OAI.JointDickman.categoricalSubsetMass, OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.categorical_bernoulli_l1_le line 147
Source documentation
The finite categorical-to-independent comparison used at a single prime. Its error is quadratic in the sum of the hit probabilities.
```
theorem categorical_bernoulli_l1_le {α : Type*} [DecidableEq α]
    (P : Finset α) (q : α → ℝ) (hq : ∀ i ∈ P, 0 ≤ q i ∧ q i ≤ 1) :
    (∑ S ∈ P.powerset, |categoricalSubsetMass P q S - bernoulliSubsetMass P q S|) ≤
      2 * (∑ i ∈ P, q i) ^ 2 := by
…
```
Mentions: OAI.JointDickman.categoricalSubsetMass, OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.categorical_bernoulli_test_bound line 157

Source documentation

Any bounded complex test inherits the same finite comparison bound.

theorem categorical_bernoulli_test_bound {α : Type*} [DecidableEq α]
    (P : Finset α) (q : α → ℝ) (hq : ∀ i ∈ P, 0 ≤ q i ∧ q i ≤ 1)
    (F : Finset α → ℂ) {L : ℝ} (hL : 0 ≤ L)
    (hF : ∀ S ∈ P.powerset, ‖F S‖ ≤ L) :
    ‖(∑ S ∈ P.powerset, (categoricalSubsetMass P q S : ℂ) * F S) -
      (∑ S ∈ P.powerset, (bernoulliSubsetMass P q S : ℂ) * F S)‖ ≤
      2 * L * (∑ i ∈ P, q i) ^ 2 := by
…

Mentions: OAI.JointDickman.categoricalSubsetMass, OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.categorical_bernoulli_uniform_l1_le line 184

Source documentation

Uniform site probabilities give the stated quadratic site-count loss.

theorem categorical_bernoulli_uniform_l1_le {α : Type*} [DecidableEq α]
    (P : Finset α) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) :
    (∑ S ∈ P.powerset,
      |categoricalSubsetMass P (fun _ => u) S - bernoulliSubsetMass P (fun _ => u) S|) ≤
      2 * (P.card : ℝ) ^ 2 * u ^ 2 := by
…

Mentions: OAI.JointDickman.categoricalSubsetMass, OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.categorical_bernoulli_prime_l1_le line 193

Source documentation

At one prime p, the local error is at most 2 |P|²/p².

theorem categorical_bernoulli_prime_l1_le {α : Type*} [DecidableEq α]
    (P : Finset α) {p : ℕ} (hp : p.Prime) :
    (∑ S ∈ P.powerset,
      |categoricalSubsetMass P (fun _ => 1 / (p : ℝ)) S -
        bernoulliSubsetMass P (fun _ => 1 / (p : ℝ)) S|) ≤
      2 * (P.card : ℝ) ^ 2 / (p : ℝ) ^ 2 := by
…

Mentions: OAI.JointDickman.categoricalSubsetMass, OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.categorical_prime_mass_nonneg line 207
Source documentation
The mutually exclusive model is a genuine nonnegative probability mass when the number of sites is at most the prime.
```
theorem categorical_prime_mass_nonneg {α : Type*} [DecidableEq α]
    (P S : Finset α) {p : ℕ} (hp : p.Prime) (hcard : P.card ≤ p) :
    0 ≤ categoricalSubsetMass P (fun _ => 1 / (p : ℝ)) S := by
…
```
Mentions: OAI.JointDickman.categoricalSubsetMass