ProductComparison.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Comparing finite product laws

Replacing one independent coordinate at a time bounds the L¹ distance of two finite product probability laws by the sum of their coordinate distances. Applied to the mutually exclusive prime-site law, this gives the accumulated quadratic error for arbitrary bounded complex tests. All identities and inequalities here are proved by finite sums.

def OAI.JointDickman.finiteProductMass line 20

Source documentation

Product mass on a finite family of coordinate spaces.

noncomputable def finiteProductMass {ι : Type*} [Fintype ι] [DecidableEq ι] {Ω : ι → Type*}
    (a : ∀ i, Ω i → ℝ) (x : ∀ i, Ω i) : ℝ := ∏ i, a i (x i)

theorem OAI.JointDickman.finiteProductMass_nonneg line 23
theorem OAI.JointDickman.finiteProductMass_sum line 28
theorem OAI.JointDickman.finiteProductMass_coordinate_l1 line 36

theorem OAI.JointDickman.finiteProductMass_l1_le line 75

Source documentation

The L¹ discrepancy of product probability masses is at most the sum of the coordinate discrepancies. No order on the coordinates is needed.

theorem finiteProductMass_l1_le {ι : Type*} [Fintype ι] [DecidableEq ι] {Ω : ι → Type*}
    [∀ i, Fintype (Ω i)] (a b : ∀ i, Ω i → ℝ)
    (ha : ∀ i x, 0 ≤ a i x) (hb : ∀ i x, 0 ≤ b i x)
    (ha1 : ∀ i, ∑ x, a i x = 1) (hb1 : ∀ i, ∑ x, b i x = 1) :
    (∑ x, |finiteProductMass a x - finiteProductMass b x|) ≤
      ∑ i, ∑ y, |a i y - b i y| := by
…

Mentions: OAI.JointDickman.finiteProductMass

theorem OAI.JointDickman.finiteProductMass_test_bound line 113

Source documentation

A bounded complex test sees no more than its bound times the sum of the coordinate L¹ errors.

theorem finiteProductMass_test_bound {ι : Type*} [Fintype ι] [DecidableEq ι] {Ω : ι → Type*}
    [∀ i, Fintype (Ω i)] (a b : ∀ i, Ω i → ℝ)
    (ha : ∀ i x, 0 ≤ a i x) (hb : ∀ i x, 0 ≤ b i x)
    (ha1 : ∀ i, ∑ x, a i x = 1) (hb1 : ∀ i, ∑ x, b i x = 1)
    (F : (∀ i, Ω i) → ℂ) {L : ℝ} (hL : 0 ≤ L) (hF : ∀ x, ‖F x‖ ≤ L) :
    ‖(∑ x, (finiteProductMass a x : ℂ) * F x) -
      (∑ x, (finiteProductMass b x : ℂ) * F x)‖ ≤
      L * ∑ i, ∑ y, |a i y - b i y| := by
…

Mentions: OAI.JointDickman.finiteProductMass

def OAI.JointDickman.categoricalProductMass line 135

Source documentation

Mutually exclusive site hits, independent between coordinates.

noncomputable def categoricalProductMass {ι α : Type*} [Fintype ι] [DecidableEq ι] [DecidableEq α]
    (P : Finset α) (q : ι → α → ℝ) (x : ι → P.powerset) : ℝ :=
…

def OAI.JointDickman.bernoulliProductMass line 140

Source documentation

Independent site hits, independent also between coordinates.

noncomputable def bernoulliProductMass {ι α : Type*} [Fintype ι] [DecidableEq ι] [DecidableEq α]
    (P : Finset α) (q : ι → α → ℝ) (x : ι → P.powerset) : ℝ :=
…

theorem OAI.JointDickman.categoricalProduct_l1_le line 144
theorem OAI.JointDickman.categoricalProduct_test_bound line 167
theorem OAI.JointDickman.prime_site_probability_square_sum line 196

theorem OAI.JointDickman.categoricalPrimeProduct_l1_le line 210

Source documentation

Accumulated prime-site discrepancy. The site count must not exceed any prime, precisely so that the categorical laws are nonnegative.

theorem categoricalPrimeProduct_l1_le {α : Type*} [DecidableEq α]
    (P : Finset α) (Q : Finset ℕ)
    (hQ : ∀ p ∈ Q, p.Prime) (hcard : ∀ p ∈ Q, P.card ≤ p) :
    (∑ x, |categoricalProductMass P (fun (p : Q) _ => 1 / (p.val : ℝ)) x -
      bernoulliProductMass P (fun (p : Q) _ => 1 / (p.val : ℝ)) x|) ≤
      2 * (P.card : ℝ) ^ 2 * ∑ p ∈ Q, 1 / (p : ℝ) ^ 2 := by
…

Mentions: OAI.JointDickman.categoricalProductMass, OAI.JointDickman.bernoulliProductMass

theorem OAI.JointDickman.categoricalPrimeProduct_test_bound line 233

Source documentation

For any bounded complex function of all prime hit sets, independent Bernoulli replacement costs at most 2 L M² sum_p 1/p².

theorem categoricalPrimeProduct_test_bound {α : Type*} [DecidableEq α]
    (P : Finset α) (Q : Finset ℕ)
    (hQ : ∀ p ∈ Q, p.Prime) (hcard : ∀ p ∈ Q, P.card ≤ p)
    (F : (Q → P.powerset) → ℂ) {L : ℝ} (hL : 0 ≤ L) (hF : ∀ x, ‖F x‖ ≤ L) :
    ‖(∑ x, (categoricalProductMass P (fun (p : Q) _ => 1 / (p.val : ℝ)) x : ℂ) * F x) -
      (∑ x, (bernoulliProductMass P (fun (p : Q) _ => 1 / (p.val : ℝ)) x : ℂ) * F x)‖ ≤
      2 * L * (P.card : ℝ) ^ 2 * ∑ p ∈ Q, 1 / (p : ℝ) ^ 2 := by
…

Mentions: OAI.JointDickman.categoricalProductMass, OAI.JointDickman.bernoulliProductMass

def OAI.JointDickman.bernoulliBitMass line 256
Source documentation
One Bernoulli coordinate, written as a mass on Bool.
```
noncomputable def bernoulliBitMass (q : ℝ) (b : Bool) : ℝ := if b then q else 1 - q
```
theorem OAI.JointDickman.bernoulliBitMass_sum line 258
theorem OAI.JointDickman.bernoulliBitMass_nonneg line 261
theorem OAI.JointDickman.bernoulliBitMass_l1 line 268
Source documentation
Changing a Bernoulli success probability has exactly this L¹ cost.
```
theorem bernoulliBitMass_l1 (q r : ℝ) :
    (∑ b, |bernoulliBitMass q b - bernoulliBitMass r b|) = 2 * |q - r| := by
…
```
Mentions: OAI.JointDickman.bernoulliBitMass
def OAI.JointDickman.subsetHitEquiv line 275
Source documentation
The membership indicators of a subset give its finite Boolean coordinates.
```
noncomputable def subsetHitEquiv {α : Type*} [DecidableEq α] (P : Finset α) :
    P.powerset ≃ (P → Bool) where
…
```
theorem OAI.JointDickman.bernoulliSubsetMass_eq_product line 295

theorem OAI.JointDickman.bernoulliSubsetMass_l1_perturb line 320

Source documentation

Independent Bernoulli subset laws are Lipschitz in their probabilities.

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

Mentions: OAI.JointDickman.bernoulliSubsetMass

theorem OAI.JointDickman.bernoulliProduct_l1_perturb line 345

Source documentation

Perturbing all prime/site probabilities costs the sum of their local probability changes, with no independence hypothesis beyond the product definition.

theorem bernoulliProduct_l1_perturb {ι α : Type*} [Fintype ι] [DecidableEq ι]
    [DecidableEq α] (P : Finset α) (q r : ι → α → ℝ)
    (hq : ∀ i j, j ∈ P → 0 ≤ q i j ∧ q i j ≤ 1)
    (hr : ∀ i j, j ∈ P → 0 ≤ r i j ∧ r i j ≤ 1) :
    (∑ x, |bernoulliProductMass P q x - bernoulliProductMass P r x|) ≤
      2 * ∑ i, ∑ j ∈ P, |q i j - r i j| := by
…

Mentions: OAI.JointDickman.bernoulliProductMass

theorem OAI.JointDickman.finiteMass_test_bound_of_l1 line 369

Source documentation

Finite L¹ error controls every bounded complex test.

theorem finiteMass_test_bound_of_l1 {Ω : Type*} [Fintype Ω]
    (a b : Ω → ℝ) (F : Ω → ℂ) {L ε : ℝ} (hL : 0 ≤ L)
    (hF : ∀ x, ‖F x‖ ≤ L) (hε : (∑ x, |a x - b x|) ≤ ε) :
    ‖(∑ x, (a x : ℂ) * F x) - (∑ x, (b x : ℂ) * F x)‖ ≤ L * ε := by
…

theorem OAI.JointDickman.bernoulliProduct_test_perturb line 384

theorem OAI.JointDickman.categoricalProduct_l1_perturb line 397

Source documentation

Mutually exclusive probabilities may also be perturbed when replacing them by independent hits. This combines the two actual comparison errors.

theorem categoricalProduct_l1_perturb {ι α : Type*} [Fintype ι] [DecidableEq ι]
    [DecidableEq α] (P : Finset α) (q r : ι → α → ℝ)
    (hq : ∀ i j, j ∈ P → 0 ≤ q i j ∧ q i j ≤ 1)
    (hr : ∀ i j, j ∈ P → 0 ≤ r i j ∧ r i j ≤ 1)
    (hsum : ∀ i, ∑ j ∈ P, q i j ≤ 1) :
    (∑ x, |categoricalProductMass P q x - bernoulliProductMass P r x|) ≤
      2 * (∑ i, (∑ j ∈ P, q i j) ^ 2) + 2 * ∑ i, ∑ j ∈ P, |q i j - r i j| := by
…

Mentions: OAI.JointDickman.categoricalProductMass, OAI.JointDickman.bernoulliProductMass

theorem OAI.JointDickman.reciprocal_exclusion_perturb line 413

Source documentation

The probability change for the extra-root model in graph.tex.

theorem reciprocal_exclusion_perturb {p M : ℝ} (hp : 0 < p) (hM : 0 ≤ M)
    (hMp : 2 * M ≤ p) : |1 / (p - M) - 1 / p| ≤ 2 * M / p ^ 2 := by
…