FairSplitChannel.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

The actual finite fair-split channel

A site is a vector of independent Bernoulli bits. Conditional on that site, each present prime is retained independently with probability one half and each absent prime stays absent. Integrating two conditionally independent retentions gives exactly the same-site two-split law, including for arbitrary output cells. This connects that law to the actual finite channel kernel.

def OAI.JointDickman.fairRetentionBitMass line 21
Source documentation
One conditional retention bit.
```
noncomputable def fairRetentionBitMass (hit retained : Bool) : ℝ :=
…
```
theorem OAI.JointDickman.fairRetentionBitMass_nonneg line 24
theorem OAI.JointDickman.fairRetentionBitMass_sum line 28
theorem OAI.JointDickman.conditionalFairSplitMass_factor line 32
Source documentation
This is the conditional independence in the definition of two fair splits.
```
theorem conditionalFairSplitMass_factor (hit b c : Bool) :
    conditionalFairSplitMass hit (b, c) =
      fairRetentionBitMass hit b * fairRetentionBitMass hit c := by
…
```
Mentions: OAI.JointDickman.conditionalFairSplitMass, OAI.JointDickman.fairRetentionBitMass
theorem OAI.JointDickman.fairRetentionBitMass_marginal line 38
def OAI.JointDickman.bernoulliSiteMass line 43
Source documentation
Independent Bernoulli mass of the original site.
```
noncomputable def bernoulliSiteMass {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (x : ι → Bool) : ℝ := finiteProductMass (fun i => bernoulliBitMass (q i)) x
```
Mentions: OAI.JointDickman.finiteProductMass, OAI.JointDickman.bernoulliBitMass
def OAI.JointDickman.fairRetentionMass line 47
Source documentation
Conditional probability of a particular retained subset of a site.
```
noncomputable def fairRetentionMass {ι : Type*} [Fintype ι] [DecidableEq ι]
    (x y : ι → Bool) : ℝ := finiteProductMass (fun i => fairRetentionBitMass (x i)) y
```
Mentions: OAI.JointDickman.finiteProductMass, OAI.JointDickman.fairRetentionBitMass
theorem OAI.JointDickman.fairRetentionMass_nonneg line 50
theorem OAI.JointDickman.fairRetentionMass_sum line 54
theorem OAI.JointDickman.bernoulliSiteMass_sum line 58
theorem OAI.JointDickman.bernoulliSiteMass_nonneg line 62

theorem OAI.JointDickman.fairRetentionMass_joint line 68

Source documentation

Summing out the shared site gives the actual joint retention law.

theorem fairRetentionMass_joint {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (y z : ι → Bool) :
    (∑ x, bernoulliSiteMass q x * fairRetentionMass x y * fairRetentionMass x z) =
      sameSiteTwoSplitProductMass q (fun i => (y i, z i)) := by
…

Mentions: OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.fairRetentionMass, OAI.JointDickman.sameSiteTwoSplitProductMass

theorem OAI.JointDickman.fairRetentionMass_marginal line 90

def OAI.JointDickman.fairSplitAverage line 101

Source documentation

Conditional expectation of a test of the retained subset.

noncomputable def fairSplitAverage {ι : Type*} [Fintype ι] [DecidableEq ι]
    (x : ι → Bool) (f : (ι → Bool) → ℝ) : ℝ := ∑ y, fairRetentionMass x y * f y

Mentions: OAI.JointDickman.fairRetentionMass

theorem OAI.JointDickman.fairSplitAverage_bilinear line 104
theorem OAI.JointDickman.fairSplitAverage_marginal line 135

def OAI.JointDickman.fairSplitTransition line 149

Source documentation

Actual transition probability to an output cell of the retained subset.

noncomputable def fairSplitTransition {ι A : Type*} [Fintype ι] [DecidableEq ι] [DecidableEq A]
    (cell : (ι → Bool) → A) (x : ι → Bool) (a : A) : ℝ := by
…

theorem OAI.JointDickman.fairSplitTransition_eq_average line 154
theorem OAI.JointDickman.fairSplitTransition_twoSplit_mass line 163

theorem OAI.JointDickman.fairSplitTransition_twoSplitKernel line 178

Source documentation

Consequently the actual finite channel's two-split kernel is the cell mass of the explicit two-split law divided by the two output atom weights.

theorem fairSplitTransition_twoSplitKernel {ι A : Type*} [Fintype ι] [DecidableEq ι] [DecidableEq A]
    (q : ι → ℝ) (cell : (ι → Bool) → A) (μ : A → ℝ) (a b : A) :
    finiteTwoSplitKernel (bernoulliSiteMass q) μ (fairSplitTransition cell) a b =
      (∑ z, if cell (fun i => (z i).1) = a ∧ cell (fun i => (z i).2) = b then
        sameSiteTwoSplitProductMass q z else 0) / (μ a * μ b) := by
…

Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.fairSplitTransition, OAI.JointDickman.sameSiteTwoSplitProductMass

def OAI.JointDickman.retainedPrimeProduct line 187
Source documentation
Prime product of one retained bit vector.
```
noncomputable def retainedPrimeProduct (Q : Finset ℕ) (y : Q → Bool) : ℕ :=
…
```
theorem OAI.JointDickman.actualSplitProducts_eq_retained line 190
def OAI.JointDickman.fairSplitPrimeCell line 196
Source documentation
The conditional probability p_A(S) that a fair split of the site has its retained prime product in the specified cell.
```
noncomputable def fairSplitPrimeCell (Q : Finset ℕ) (A : Set ℕ) (x : Q → Bool) : ℝ := by
…
```
theorem OAI.JointDickman.fairSplitPrimeCell_eq line 201
theorem OAI.JointDickman.fairSplitPrimeCell_joint line 212
Source documentation
The actual fair-split channel numerator equals the cell mass of the two-split prime-product law. The equality holds for any site probabilities.
```
theorem fairSplitPrimeCell_joint (Q : Finset ℕ) (q : Q → ℝ) (A B : Set ℕ) :
    (∑ x, bernoulliSiteMass q x * fairSplitPrimeCell Q A x * fairSplitPrimeCell Q B x) =
      ∑ z, if (actualSplitProducts Q z).1 ∈ A ∧ (actualSplitProducts Q z).2 ∈ B then
        sameSiteTwoSplitProductMass q z else 0 := by
…
```
Mentions: OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.fairSplitPrimeCell, OAI.JointDickman.actualSplitProducts, OAI.JointDickman.sameSiteTwoSplitProductMass
theorem OAI.JointDickman.fairSplitPrimeCell_marginal line 227
Source documentation
A single fair split changes the prime-site probabilities from 1/p to 1/(2p), exactly and before any prime asymptotics.
```
theorem fairSplitPrimeCell_marginal (Q : Finset ℕ) (A : Set ℕ) :
    (∑ x, bernoulliSiteMass (fun p : Q => 1 / (p.val : ℝ)) x * fairSplitPrimeCell Q A x) =
      ∑ y, if retainedPrimeProduct Q y ∈ A then
        bernoulliSiteMass (fun p : Q => 1 / (2 * (p.val : ℝ))) y else 0 := by
…
```
Mentions: OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.fairSplitPrimeCell, OAI.JointDickman.retainedPrimeProduct
theorem OAI.JointDickman.fairPrimeTransition_twoSplitKernel line 244
Source documentation
Kernel identity for any finite partition of the retained prime product. This is the direct bridge from the actual channel to two-split cell estimates.
```
theorem fairPrimeTransition_twoSplitKernel {A : Type*} [DecidableEq A]
    (Q : Finset ℕ) (q : Q → ℝ) (cell : ℕ → A) (μ : A → ℝ) (a b : A) :
    finiteTwoSplitKernel (bernoulliSiteMass q) μ
      (fairSplitTransition (fun y => cell (retainedPrimeProduct Q y))) a b =
      (∑ z, if cell (actualSplitProducts Q z).1 = a ∧ cell (actualSplitProducts Q z).2 = b then
        sameSiteTwoSplitProductMass q z else 0) / (μ a * μ b) := by
…
```
Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.fairSplitTransition, OAI.JointDickman.retainedPrimeProduct, OAI.JointDickman.actualSplitProducts, OAI.JointDickman.sameSiteTwoSplitProductMass