IndependentKernelSplit.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

The independent common/exclusive model and its cutoff

The three independent category bits are reindexed as three independent Boolean prime subsets. Their products are the common product and the two exclusive products. The low-exclusive union is separated exactly; the complement is the product of the two high-exclusive cell probabilities.

def OAI.JointDickman.categoryToTriple line 20
def OAI.JointDickman.tripleToCategory line 24
theorem OAI.JointDickman.tripleToCategory_categoryToTriple line 29
theorem OAI.JointDickman.categoryToTriple_tripleToCategory line 36
def OAI.JointDickman.categoryTripleEquiv line 42
Source documentation
Three category bits at each site are exactly three Boolean vectors.
```
def categoryTripleEquiv (ι : Type*) :
    (ι → SplitCategories) ≃ (ι → Bool) × (ι → Bool) × (ι → Bool) where
…
```
Mentions: OAI.JointDickman.SplitCategories

theorem OAI.JointDickman.independentCategoryMass_triple line 61

Source documentation

The independent category weight factors into the three actual Bernoulli subset weights, without a coupling assumption.

theorem independentCategoryMass_triple {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (y : ι → SplitCategories) :
    bernoulliProductMass Finset.univ (fun i (_ : Fin 3) => q i) y =
      bernoulliSiteMass q ((categoryTripleEquiv ι y).1) *
      bernoulliSiteMass q ((categoryTripleEquiv ι y).2.1) *
      bernoulliSiteMass q ((categoryTripleEquiv ι y).2.2) :=
…

Mentions: OAI.JointDickman.SplitCategories, OAI.JointDickman.bernoulliProductMass, OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.categoryTripleEquiv

theorem OAI.JointDickman.independentCategory_triple_test line 70

Source documentation

Exact real-test pushforward to the independent triple law.

theorem independentCategory_triple_test {ι : Type*} [Fintype ι] [DecidableEq ι]
    (q : ι → ℝ) (F : (ι → Bool) → (ι → Bool) → (ι → Bool) → ℝ) :
    (∑ y, bernoulliProductMass Finset.univ (fun i (_ : Fin 3) => q i) y *
      F ((categoryTripleEquiv ι y).1) ((categoryTripleEquiv ι y).2.1)
        ((categoryTripleEquiv ι y).2.2)) =
      ∑ c, ∑ e₁, ∑ e₂,
        bernoulliSiteMass q c * bernoulliSiteMass q e₁ * bernoulliSiteMass q e₂ * F c e₁ e₂ := by
…

Mentions: OAI.JointDickman.bernoulliProductMass, OAI.JointDickman.categoryTripleEquiv, OAI.JointDickman.bernoulliSiteMass

theorem OAI.JointDickman.categoryPrimeProduct_eq_retained line 83
def OAI.JointDickman.independentPairMass line 96
theorem OAI.JointDickman.independentPairMass_eq_triple line 100

def OAI.JointDickman.lowUnionExclusiveMass line 118

Source documentation

The discarded mass is the genuine union event, so overlap is counted once.

noncomputable def lowUnionExclusiveMass (w : C → ℝ) (v : E → ℝ)
    (cell : C → E → Option A) (low : E → Prop) [DecidablePred low] (a b : A) : ℝ :=
…

def OAI.JointDickman.highExclusiveCell line 125

Source documentation

Conditional cell probability retaining only high exclusive products.

noncomputable def highExclusiveCell (v : E → ℝ) (cell : C → E → Option A)
    (low : E → Prop) [DecidablePred low] (c : C) (a : A) : ℝ :=
…

theorem OAI.JointDickman.highExclusiveCell_eq_sum line 130
theorem OAI.JointDickman.highExclusiveCell_nonneg line 140
theorem OAI.JointDickman.highExclusiveCell_le_one line 148

theorem OAI.JointDickman.independentPairMass_cutoff line 157

Source documentation

The high-high complement factors after conditioning on the common variable.

theorem independentPairMass_cutoff (w : C → ℝ) (v : E → ℝ)
    (cell : C → E → Option A) (low : E → Prop) [DecidablePred low] (a b : A) :
    independentPairMass w v cell a b = lowUnionExclusiveMass w v cell low a b +
      ∑ c, w c * highExclusiveCell v cell low c a * highExclusiveCell v cell low c b := by
…

Mentions: OAI.JointDickman.independentPairMass, OAI.JointDickman.lowUnionExclusiveMass, OAI.JointDickman.highExclusiveCell

theorem OAI.JointDickman.lowUnionExclusiveMass_nonneg line 181

theorem OAI.JointDickman.lowUnionExclusiveMass_le_sides line 194

Source documentation

The low union is dominated by the two one-sided low kernels.

theorem lowUnionExclusiveMass_le_sides (w : C → ℝ) (v : E → ℝ)
    (cell : C → E → Option A) (low : E → Prop) [DecidablePred low]
    (hw : ∀ c, 0 ≤ w c) (hv : ∀ e, 0 ≤ v e) (a b : A) :
    lowUnionExclusiveMass w v cell low a b ≤
      lowExclusiveMass w v cell low a b + lowExclusiveMass w v cell low b a := by
…

Mentions: OAI.JointDickman.lowUnionExclusiveMass, OAI.JointDickman.lowExclusiveMass

def OAI.JointDickman.lowUnionExclusiveKernel line 217
theorem OAI.JointDickman.lowUnionExclusiveKernel_nonneg line 221

theorem OAI.JointDickman.lowUnionExclusiveKernel_weighted_rows line 230

Source documentation

Local marginal and conditional common-cell bounds control the actual union kernel, including the overlap of its two low-exclusive events.

theorem lowUnionExclusiveKernel_weighted_rows [Fintype A]
    (w : C → ℝ) (v : E → ℝ) (cell : C → E → Option A)
    (low : E → Prop) [DecidablePred low]
    (hw : ∀ c, 0 ≤ w c) (hv : ∀ e, 0 ≤ v e) (hv1 : ∑ e, v e = 1)
    {m H : ℝ} (hm : 0 < m)
    (hmarginal : ∀ a, independentCellMarginal w v cell a ≤ H * m)
    (hcommon : ∀ e, low e → ∀ b, optionCellMass w (fun c => cell c e) b ≤ H * m)
    (a : A) :
    (∑ b, m * lowUnionExclusiveKernel w v cell low (fun _ => m) a b) ≤
      2 * lowExclusiveProbability v low * H := by
…

Mentions: OAI.JointDickman.independentCellMarginal, OAI.JointDickman.optionCellMass, OAI.JointDickman.lowUnionExclusiveKernel, OAI.JointDickman.lowExclusiveProbability

def OAI.JointDickman.primeProductCell line 268

theorem OAI.JointDickman.independentPrimeCellMass_eq_pair line 272

Source documentation

Exact cell-pair probabilities under the independent prime-category law.

theorem independentPrimeCellMass_eq_pair {A : Type*} [DecidableEq A]
    (Q : Finset ℕ) (q : Q → ℝ) (cell : ℕ → Option A) (a b : A) :
    (∑ y, if cell (independentSplitProducts Q y).1 = some a ∧
        cell (independentSplitProducts Q y).2 = some b then
      bernoulliProductMass Finset.univ (fun p (_ : Fin 3) => q p) y else 0) =
      independentPairMass (bernoulliSiteMass q) (bernoulliSiteMass q)
        (primeProductCell Q cell) a b := by
…

Mentions: OAI.JointDickman.independentSplitProducts, OAI.JointDickman.bernoulliProductMass, OAI.JointDickman.independentPairMass, OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.primeProductCell

theorem OAI.JointDickman.independentPairKernel_cutoff line 302

Source documentation

Normalize the exact cutoff identity by the actual output cell masses.

theorem independentPairKernel_cutoff {C E D R : Type*}
    [Fintype C] [Fintype E] [DecidableEq D] [DecidableEq R]
    (w : C → ℝ) (v : E → ℝ) (cell : C → E → Option (D × R))
    (low : E → Prop) [DecidablePred low] (μ : D → ℝ) (a b : D × R) :
    independentPairMass w v cell a b / (μ a.1 * μ b.1) =
      lowUnionExclusiveKernel w v cell low (fun a : D × R => μ a.1) a b +
      exclusiveProductKernel w μ (highExclusiveCell v cell low) a b := by
…

Mentions: OAI.JointDickman.independentPairMass, OAI.JointDickman.lowUnionExclusiveKernel, OAI.JointDickman.exclusiveProductKernel, OAI.JointDickman.highExclusiveCell

theorem OAI.JointDickman.independentPrimeKernel_cutoff line 314

Source documentation

The independent category kernel has exactly the low-union plus high-exclusive-product decomposition needed by residue flattening.

theorem independentPrimeKernel_cutoff {D R : Type*} [DecidableEq D] [DecidableEq R]
    (Q : Finset ℕ) (q : Q → ℝ) (cell : ℕ → Option (D × R))
    (low : (Q → Bool) → Prop) [DecidablePred low] (μ : D → ℝ) (a b : D × R) :
    (∑ y, if cell (independentSplitProducts Q y).1 = some a ∧
        cell (independentSplitProducts Q y).2 = some b then
      bernoulliProductMass Finset.univ (fun p (_ : Fin 3) => q p) y else 0) /
        (μ a.1 * μ b.1) =
      lowUnionExclusiveKernel (bernoulliSiteMass q) (bernoulliSiteMass q)
        (primeProductCell Q cell) low (fun a : D × R => μ a.1) a b +
      exclusiveProductKernel (bernoulliSiteMass q) μ
        (highExclusiveCell (bernoulliSiteMass q) (primeProductCell Q cell) low) a b := by
…

Mentions: OAI.JointDickman.independentSplitProducts, OAI.JointDickman.bernoulliProductMass, OAI.JointDickman.lowUnionExclusiveKernel, OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.primeProductCell, OAI.JointDickman.exclusiveProductKernel, OAI.JointDickman.highExclusiveCell