FiniteProbability.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted sampling for the random-prime rank argument

The prime labels in the rank argument have a nonuniform reciprocal law. The corresponding finite-sum probability identities account for that law.

structure OAI.TwoPointCorrelations.FiniteLaw line 19
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:19 (same declaration text).
def OAI.TwoPointCorrelations.FiniteLaw.average line 28
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:28 (same declaration text).
def OAI.TwoPointCorrelations.FiniteLaw.probability line 31
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.average_nonneg line 35
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:35 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.average_mono line 38
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:38 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.average_const line 41
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:41 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.average_sum line 44
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:44 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.average_mul_const line 49
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:49 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.average_comm line 53
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:53 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.square_average_le line 64
Source documentation
Weighted Cauchy--Schwarz against the constant function one.
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:64 (same declaration text).
```
lemma square_average_le (μ : FiniteLaw α) (f : α → ℝ) :
    (μ.average f) ^ 2 ≤ μ.average (fun x => f x ^ 2) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw
lemma OAI.TwoPointCorrelations.FiniteLaw.square_average_eq line 74
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:74 (same declaration text).
theorem OAI.TwoPointCorrelations.FiniteLaw.two_sample_bound line 85
Source documentation
Repeating the second sample removes every term depending only on the first sample. This is the Cauchy--Schwarz step of q:rank-probability.
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:85 (same declaration text).
```
theorem two_sample_bound (μ : FiniteLaw α) (ν : FiniteLaw β)
    (E : α → β → Prop) (D : α → β → β → Prop)
    (hD : ∀ c y z, E c y → E c z → D c y z) :
    (μ.average (fun c => ν.probability (E c))) ^ 2 ≤
      μ.average (fun c => ν.average (fun y => ν.probability (D c y))) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw
def OAI.TwoPointCorrelations.FiniteLaw.product line 105
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:105 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.average_product line 110
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:110 (same declaration text).
def OAI.TwoPointCorrelations.FiniteLaw.independent line 114
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:114 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_product line 121
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:121 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.probability_nonneg line 126
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:126 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.probability_le_one line 132
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:132 (same declaration text).
lemma OAI.TwoPointCorrelations.FiniteLaw.probability_le_atom_bound line 140
Source documentation
If an event contains at most one atom, its mass is bounded by the largest allowed atom. This is used after fixing the nonpivot labels.
Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteProbability.lean:140 (same declaration text).
```
lemma probability_le_atom_bound (μ : FiniteLaw α) (E : α → Prop) (a : ℝ)
    (ha : 0 ≤ a) (hatom : ∀ x, μ.weight x ≤ a)
    (hunique : ∀ x y, E x → E y → x = y) : μ.probability E ≤ a := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw