TwoSplitLaw.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Two fair splits of the same prime site

The local law is constructed by first selecting a Bernoulli site and then, conditional on that hit, taking two independent fair splits. Its common and exclusive categories have mass q/4 each. Finite product comparison gives the independent common/exclusive model without assuming a coupling.

def OAI.JointDickman.finitePushMass line 19

Source documentation

Finite pushforward of a real mass function.

noncomputable def finitePushMass {A B : Type*} [Fintype A]
    (a : A → ℝ) (f : A → B) (y : B) : ℝ := by
…

theorem OAI.JointDickman.finitePushMass_test line 24

theorem OAI.JointDickman.finiteProductMass_pushforward line 43

Source documentation

Pushforward commutes with finite independent products.

theorem finiteProductMass_pushforward {ι : Type*} [Fintype ι] [DecidableEq ι]
    {A B : ι → Type*} [∀ i, Fintype (A i)] [∀ i, Fintype (B i)]
    (a : ∀ i, A i → ℝ) (f : ∀ i, A i → B i) (y : ∀ i, B i) :
    finiteProductMass (fun i => finitePushMass (a i) (f i)) y =
      finitePushMass (finiteProductMass a) (fun x i => f i (x i)) y := by
…

Mentions: OAI.JointDickman.finiteProductMass, OAI.JointDickman.finitePushMass

theorem OAI.JointDickman.finiteProductMass_pushforward_test line 66
def OAI.JointDickman.conditionalFairSplitMass line 76
Source documentation
Conditional on a site hit, the two choices are independent fair bits; an absent site gives two absent splits.
```
noncomputable def conditionalFairSplitMass (hit : Bool) (b : Bool × Bool) : ℝ :=
…
```
def OAI.JointDickman.sameSiteTwoSplitMass line 81
Source documentation
The actual same-site two-split law, integrating out the Bernoulli hit.
```
noncomputable def sameSiteTwoSplitMass (q : ℝ) (b : Bool × Bool) : ℝ :=
…
```
theorem OAI.JointDickman.conditionalFairSplitMass_sum line 84
theorem OAI.JointDickman.sameSiteTwoSplitMass_formula line 88
theorem OAI.JointDickman.sameSiteTwoSplitMass_sum line 94
theorem OAI.JointDickman.sameSiteTwoSplitMass_nonneg line 99
abbrev OAI.JointDickman.SplitCategories line 105
Source documentation
The three labels are common, first-exclusive, second-exclusive.
```
abbrev SplitCategories := ((Finset.univ : Finset (Fin 3)).powerset : Type)
```
def OAI.JointDickman.splitCategory line 107
theorem OAI.JointDickman.sameSiteTwoSplitMass_categories line 117
Source documentation
This identifies the categorical law from the actual conditional split construction, including its empty-set mass.
```
theorem sameSiteTwoSplitMass_categories (q : ℝ) (S : SplitCategories) :
    finitePushMass (sameSiteTwoSplitMass q) splitCategory S =
      categoricalSubsetMass Finset.univ (fun _ : Fin 3 => q / 4) S.val := by
…
```
Mentions: OAI.JointDickman.SplitCategories, OAI.JointDickman.finitePushMass, OAI.JointDickman.sameSiteTwoSplitMass, OAI.JointDickman.splitCategory, OAI.JointDickman.categoricalSubsetMass
theorem OAI.JointDickman.threeCategoryBernoulli_factor line 124

theorem OAI.JointDickman.independentCategoryProductMass_factor line 141

Source documentation

The comparison law really is a product of the three category vectors, each of which is itself a product of Bernoulli coordinates.

theorem independentCategoryProductMass_factor {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (y : ι → SplitCategories) :
    bernoulliProductMass Finset.univ (fun i (_ : Fin 3) => q i) y =
      finiteProductMass (fun i => bernoulliBitMass (q i)) (fun i => decide ((0 : Fin 3) ∈ (y i).val)) *
      finiteProductMass (fun i => bernoulliBitMass (q i)) (fun i => decide ((1 : Fin 3) ∈ (y i).val)) *
      finiteProductMass (fun i => bernoulliBitMass (q i)) (fun i => decide ((2 : Fin 3) ∈ (y i).val)) := by
…

Mentions: OAI.JointDickman.SplitCategories, OAI.JointDickman.bernoulliProductMass, OAI.JointDickman.finiteProductMass, OAI.JointDickman.bernoulliBitMass

def OAI.JointDickman.sameSiteTwoSplitProductMass line 152

Source documentation

Product law of the actual pairs of fair splits.

noncomputable def sameSiteTwoSplitProductMass {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (x : ι → Bool × Bool) : ℝ :=
…

theorem OAI.JointDickman.sameSiteTwoSplitProductMass_sum line 156
theorem OAI.JointDickman.sameSiteTwoSplitProductMass_nonneg line 160
theorem OAI.JointDickman.sameSiteTwoSplitProduct_categories line 165

theorem OAI.JointDickman.sameSiteTwoSplitProduct_test_bound line 176

Source documentation

Comparing the actual two-split law to three independent category bits.

theorem sameSiteTwoSplitProduct_test_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (hq : ∀ i, 0 ≤ q i ∧ q i ≤ 1)
    (F : (ι → SplitCategories) → ℂ) {L : ℝ} (hL : 0 ≤ L) (hF : ∀ y, ‖F y‖ ≤ L) :
    ‖(∑ x, (sameSiteTwoSplitProductMass q x : ℂ) * F (fun i => splitCategory (x i))) -
      (∑ y, (bernoulliProductMass Finset.univ (fun i (_ : Fin 3) => q i / 4) y : ℂ) * F y)‖ ≤
      (9 / 8 : ℝ) * L * ∑ i, (q i) ^ 2 := by
…

Mentions: OAI.JointDickman.SplitCategories, OAI.JointDickman.sameSiteTwoSplitProductMass, OAI.JointDickman.splitCategory, OAI.JointDickman.bernoulliProductMass

theorem OAI.JointDickman.sameSiteTwoSplitPrime_test_bound line 203

Source documentation

Prime-site specialization with the explicit 9/8 coefficient.

theorem sameSiteTwoSplitPrime_test_bound (Q : Finset ℕ)
    (hQ : ∀ p ∈ Q, p.Prime) (F : (Q → SplitCategories) → ℂ)
    {L : ℝ} (hL : 0 ≤ L) (hF : ∀ y, ‖F y‖ ≤ L) :
    ‖(∑ x, (sameSiteTwoSplitProductMass (fun p : Q => 1 / (p.val : ℝ)) x : ℂ) *
        F (fun p => splitCategory (x p))) -
      (∑ y, (bernoulliProductMass Finset.univ
        (fun (p : Q) (_ : Fin 3) => 1 / (4 * (p.val : ℝ))) y : ℂ) * F y)‖ ≤
      (9 / 8 : ℝ) * L * ∑ p ∈ Q, 1 / (p : ℝ) ^ 2 := by
…

Mentions: OAI.JointDickman.SplitCategories, OAI.JointDickman.sameSiteTwoSplitProductMass, OAI.JointDickman.splitCategory, OAI.JointDickman.bernoulliProductMass

def OAI.JointDickman.categoryPrimeProduct line 224
Source documentation
Prime product corresponding to one of the common/exclusive categories.
```
noncomputable def categoryPrimeProduct (Q : Finset ℕ) (k : Fin 3)
    (y : Q → SplitCategories) : ℕ :=
…
```
Mentions: OAI.JointDickman.SplitCategories
def OAI.JointDickman.independentSplitProducts line 230
Source documentation
The independent model is (C E₁, C E₂). If two categories contain the same prime, its square is retained in the corresponding product.
```
noncomputable def independentSplitProducts (Q : Finset ℕ) (y : Q → SplitCategories) : ℕ × ℕ :=
…
```
Mentions: OAI.JointDickman.SplitCategories
def OAI.JointDickman.actualSplitProducts line 235
Source documentation
Prime products of the actual pair of splits.
```
noncomputable def actualSplitProducts (Q : Finset ℕ) (x : Q → Bool × Bool) : ℕ × ℕ :=
…
```
theorem OAI.JointDickman.independentSplitProducts_of_actual line 238

theorem OAI.JointDickman.twoSplitPrimeProducts_test_bound line 259

Source documentation

The manuscript's two-split comparison, directly for arbitrary bounded tests of the resulting pair of prime products. It applies in particular to every pair of cells used in the step kernel.

theorem twoSplitPrimeProducts_test_bound (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
    (F : ℕ × ℕ → ℂ) {L : ℝ} (hL : 0 ≤ L) (hF : ∀ z, ‖F z‖ ≤ L) :
    ‖(∑ x, (sameSiteTwoSplitProductMass (fun p : Q => 1 / (p.val : ℝ)) x : ℂ) *
        F (actualSplitProducts Q x)) -
      (∑ y, (bernoulliProductMass Finset.univ
        (fun (p : Q) (_ : Fin 3) => 1 / (4 * (p.val : ℝ))) y : ℂ) *
          F (independentSplitProducts Q y))‖ ≤
      (9 / 8 : ℝ) * L * ∑ p ∈ Q, 1 / (p : ℝ) ^ 2 := by
…

Mentions: OAI.JointDickman.sameSiteTwoSplitProductMass, OAI.JointDickman.actualSplitProducts, OAI.JointDickman.bernoulliProductMass, OAI.JointDickman.independentSplitProducts

theorem OAI.JointDickman.twoSplitPrimeProducts_cell_bound line 273

Source documentation

The cell-pair probability estimate used to compare step kernels.

theorem twoSplitPrimeProducts_cell_bound (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime)
    (A B : Set ℕ) :
    |(∑ x, if (actualSplitProducts Q x).1 ∈ A ∧ (actualSplitProducts Q x).2 ∈ B then
        sameSiteTwoSplitProductMass (fun p : Q => 1 / (p.val : ℝ)) x else 0) -
      (∑ y, if (independentSplitProducts Q y).1 ∈ A ∧ (independentSplitProducts Q y).2 ∈ B then
        bernoulliProductMass Finset.univ
          (fun (p : Q) (_ : Fin 3) => 1 / (4 * (p.val : ℝ))) y else 0)| ≤
      (9 / 8 : ℝ) * ∑ p ∈ Q, 1 / (p : ℝ) ^ 2 := by
…

Mentions: OAI.JointDickman.actualSplitProducts, OAI.JointDickman.sameSiteTwoSplitProductMass, OAI.JointDickman.independentSplitProducts, OAI.JointDickman.bernoulliProductMass