SignedChannelMass.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of signed split masses and the actual channel

def OAI.JointDickman.primeSplitProductSupport line 11
def OAI.JointDickman.subsetSiteTest line 14
theorem OAI.JointDickman.retainedPrimeProduct_subset line 17
theorem OAI.JointDickman.fullPrimeMass_subset line 27

theorem OAI.JointDickman.signedSplitProductMass_sum line 35

Source documentation

Push the finite signed split measure forward to its integer product.

theorem signedSplitProductMass_sum (P : Finset ℕ) (g : Finset ℕ → ℝ) (F : ℕ → ℝ) :
    (∑ n ∈ primeSplitProductSupport P, signedSplitProductMass P g n * F n) =
      ∑ S ∈ P.powerset, bernoulliSubsetMass P (fun p => 1/(p : ℝ)) S * g S *
        ∑ A ∈ P.powerset, subsetRetentionMass S A * F (∏ p ∈ A, p) := by
…

Mentions: OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.subsetRetentionMass

theorem OAI.JointDickman.signedSplitProductMass_expectation line 58
Source documentation
The signed integer-product law is exactly the original fair-split expectation.
```
theorem signedSplitProductMass_expectation (P : Finset ℕ)
    (g : (P → Bool) → ℝ) (F : ℕ → ℝ) :
    (∑ n ∈ primeSplitProductSupport P,
      signedSplitProductMass P (subsetSiteTest P g) n * F n) =
      ∑ x : P → Bool, fullPrimeMass P x * g x *
        ∑ y : P → Bool, fairRetentionMass x y * F (retainedPrimeProduct P y) := by
…
```
Mentions: OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.subsetSiteTest, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.fairRetentionMass, OAI.JointDickman.retainedPrimeProduct

theorem OAI.JointDickman.signedSplitProductMass_channel line 78

Source documentation

A channel cell contains exactly the corresponding signed integer masses.

theorem signedSplitProductMass_channel {A : Type*} [Fintype A] [DecidableEq A]
    (P : Finset ℕ) (g : (P → Bool) → ℝ) (cell : ℕ → Option A)
    (μ : A → ℝ) (a : A) (hμ : μ a ≠ 0) :
    (∑ n ∈ primeSplitProductSupport P, if cell n = some a then
      signedSplitProductMass P (subsetSiteTest P g) n else 0) =
      μ a * finiteChannel (fullPrimeMass P) μ (partialFairPrimeTransition P cell) g a := by
…

Mentions: OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.subsetSiteTest, OAI.JointDickman.finiteChannel, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.partialFairPrimeTransition

theorem OAI.JointDickman.manuscriptChannel_cell_mass line 95

Source documentation

The manuscript normalization is delta/phi, with no approximation.

theorem manuscriptChannel_cell_mass {m₁ B q : ℕ} [NeZero q]
    (hm : 0 < m₁) (hB : 0 < B) (g : (auxiliaryPrimes B → Bool) → ℝ)
    (a : Fin (channelFineCount m₁ B) × (ZMod q)ˣ) :
    (∑ n ∈ primeSplitProductSupport (auxiliaryPrimes B),
      if logResidueCell B q (channelLower (channelFineCount m₁ B))
        (channelUpper (channelFineCount m₁ B)) n = some a then
        signedSplitProductMass (auxiliaryPrimes B) (subsetSiteTest (auxiliaryPrimes B) g) n
      else 0) =
      (channelMesh (channelFineCount m₁ B)/(q.totient : ℝ))*
        manuscriptChannel m₁ B q g a := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.channelFineCount, OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.logResidueCell, OAI.JointDickman.channelLower, OAI.JointDickman.channelUpper, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.subsetSiteTest, OAI.JointDickman.channelMesh, OAI.JointDickman.manuscriptChannel