Random.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct line 16
Source documentation
Product of the independent Bernoulli trials in the source table model.
```
def bernoulliProduct {I : Type*} [Fintype I] [DecidableEq I] (p : I → ℝ)
    (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) : FiniteLaw (I → Bool) where
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw
lemma OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct_expect_product line 27

lemma OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct_all line 38

Source documentation

Probability of simultaneous inclusion for any specified, distinct trials.

lemma bernoulliProduct_all {I : Type*} [Fintype I] [DecidableEq I]
    (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) (s : Finset I) :
    (bernoulliProduct p hp).expect (fun w => if ∀ i ∈ s, w i = true then 1 else 0) =
      ∏ i ∈ s, p i := by
…

Mentions: OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.FiniteLaw.expect

def OAI.HyperbolicObstruction.FiniteLaw.prob line 58
Source documentation
Probability, in real rather than ENNReal coordinates, of a finite event.
```
def prob (μ : FiniteLaw α) (E : α → Prop) [DecidablePred E] : ℝ :=
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw
lemma OAI.HyperbolicObstruction.FiniteLaw.prob_nonneg line 61
lemma OAI.HyperbolicObstruction.FiniteLaw.prob_le_one line 66

lemma OAI.HyperbolicObstruction.FiniteLaw.prob_exists_le line 78

Source documentation

The finite union bound; no independence is assumed here.

lemma prob_exists_le {J : Type*} [Fintype J] (μ : FiniteLaw α)
    (E : J → α → Prop) [∀ j, DecidablePred (E j)] :
    μ.prob (fun a => ∃ j, E j a) ≤ ∑ j, μ.prob (E j) := by
…

Mentions: OAI.HyperbolicObstruction.FiniteLaw

abbrev OAI.HyperbolicObstruction.TableModel.Entry line 104
Source documentation
Each table has a distinct type, but all its coordinate fields use the same alphabet. Coinciding numerical values at different fields are permitted.
```
abbrev Entry (support : R → Finset F) := Σ r, (support r → A)
```
def OAI.HyperbolicObstruction.TableModel.row line 106
lemma OAI.HyperbolicObstruction.TableModel.row_injective line 110
def OAI.HyperbolicObstruction.TableModel.law line 115
def OAI.HyperbolicObstruction.TableModel.IsMatch line 120
instance OAI.HyperbolicObstruction.TableModel.(instance at line 123) line 123
theorem OAI.HyperbolicObstruction.TableModel.prob_isMatch line 129
Source documentation
A master assignment uses exactly one trial of each distinct array. Hence its inclusion probability is independent of every letter value and collision.
```
theorem prob_isMatch (support : R → Finset F) (p : R → ℝ)
    (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) (σ : F → A) :
    (law support p hp).prob (fun w => IsMatch support w σ) = ∏ r, p r := by
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.law, OAI.HyperbolicObstruction.TableModel.IsMatch
def OAI.HyperbolicObstruction.TableModel.matchCount line 142
Source documentation
The number of master matches for the given finite table instance.
```
def matchCount (support : R → Finset F) (w : Entry (A := A) support → Bool) : ℕ :=
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry
theorem OAI.HyperbolicObstruction.TableModel.expect_matchCount line 147
Source documentation
Exact first moment. No asymptotic approximation or injectivity restriction on a match is involved, as in source Equation sample:eq-master-mean.
```
theorem expect_matchCount (support : R → Finset F) (p : R → ℝ)
    (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) :
    (law (A := A) support p hp).expect (fun w => (matchCount support w : ℝ)) =
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.law, OAI.HyperbolicObstruction.TableModel.matchCount
def OAI.HyperbolicObstruction.TableModel.overlapRows line 177
Source documentation
The common entries of two master assignments, counted by array type.
```
def overlapRows (support : R → Finset F) (σ τ : F → A) : Finset R :=
…
```
lemma OAI.HyperbolicObstruction.TableModel.overlap_image line 181
theorem OAI.HyperbolicObstruction.TableModel.prob_pair_mul_overlap line 199
Source documentation
Exact joint-inclusion identity, retaining the recoverable cost of every shared entry. Different fields with equal numerical values are not identified.
```
theorem prob_pair_mul_overlap (support : R → Finset F) (p : R → ℝ)
    (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) (σ τ : F → A) :
    (law support p hp).prob (fun w => IsMatch support w σ ∧ IsMatch support w τ) *
      (∏ r ∈ overlapRows support σ τ, p r) = (∏ r, p r) ^ 2 := by
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.law, OAI.HyperbolicObstruction.TableModel.IsMatch, OAI.HyperbolicObstruction.TableModel.overlapRows
theorem OAI.HyperbolicObstruction.TableModel.prob_pair line 230
Source documentation
Inclusion ratio agrees exactly with the product of reciprocal shared-entry probabilities. Positivity is retained, rather than silently cancelling zero.
```
theorem prob_pair (support : R → Finset F) (p : R → ℝ)
    (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) (hpos : ∀ r, 0 < p r) (σ τ : F → A) :
    (law support p hp).prob (fun w => IsMatch support w σ ∧ IsMatch support w τ) =
      (∏ r, p r) ^ 2 / (∏ r ∈ overlapRows support σ τ, p r) := by
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.law, OAI.HyperbolicObstruction.TableModel.IsMatch, OAI.HyperbolicObstruction.TableModel.overlapRows
theorem OAI.HyperbolicObstruction.TableModel.expect_matchCount_sq line 239
Source documentation
Turning the square of the match count into ordered pairs is exact for every finite table instance.
```
theorem expect_matchCount_sq (support : R → Finset F) (p : R → ℝ)
    (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) :
    (law (A := A) support p hp).expect (fun w => (matchCount support w : ℝ) ^ 2) =
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.law, OAI.HyperbolicObstruction.TableModel.matchCount
lemma OAI.HyperbolicObstruction.TableModel.sum_coincidence line 276
Source documentation
Coincidence counting uses equality only within each coordinate field; the letters in other fields range independently over the very same alphabet.
```
lemma sum_coincidence (σ : F → A) (W : Finset F) :
    (∑ τ : F → A, if ∀ i ∈ W, τ i = σ i then (1 : ℝ) else 0) =
      (Fintype.card A : ℝ) ^ (Fintype.card F - W.card) := by
…
```
lemma OAI.HyperbolicObstruction.TableModel.row_eq_iff line 296
lemma OAI.HyperbolicObstruction.TableModel.rows_eq_iff line 307
lemma OAI.HyperbolicObstruction.TableModel.inverse_overlap_expansion line 322
Source documentation
Exact expansion of the pair-inclusion ratio by subsets of the shared row types. This form permits counting prescribed coordinate equalities rather than making an incorrect disjoint-domain assumption.
```
lemma inverse_overlap_expansion (support : R → Finset F) (p : R → ℝ)
    (σ τ : F → A) :
    (∏ r ∈ overlapRows support σ τ, p r)⁻¹ =
      ∑ J : Finset R, if ∀ i ∈ J.biUnion support, σ i = τ i then
        ∏ r ∈ J, ((p r)⁻¹ - 1) else 0 := by
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.overlapRows

lemma OAI.HyperbolicObstruction.TableModel.sum_inverse_overlap line 352

Source documentation

Summing the exact overlap identity over the second assignment.

lemma sum_inverse_overlap (support : R → Finset F) (p : R → ℝ) (σ : F → A) :
    (∑ τ : F → A, (∏ r ∈ overlapRows support σ τ, p r)⁻¹) =
      ∑ J : Finset R, (Fintype.card A : ℝ) ^ (Fintype.card F - (J.biUnion support).card) *
        ∏ r ∈ J, ((p r)⁻¹ - 1) := by
…

Mentions: OAI.HyperbolicObstruction.TableModel.overlapRows