BinomialMixture.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.MatroidProphet.SecretaryBinomialMixture.bitsWeight_const line 18
Source documentation
A homogeneous Bernoulli mask has the exact cardinality-dependent mass.
```
lemma bitsWeight_const (p : ℝ) (V S : Finset α) (hS : S ⊆ V) :
    bitsWeight (fun _ => p) V S = p ^ S.card * (1 - p) ^ (V.card - S.card) := by
…
```
Mentions: OAI.MatroidProphet.bitsWeight
theorem OAI.MatroidProphet.SecretaryBinomialMixture.bitsExpectation_card line 34
Source documentation
The cardinality of a predrawn product mask has the full binomial law. The identity also holds at p = 0, p = 1, and for an empty ground set.
```
theorem bitsExpectation_card (p : ℝ) (V : Finset α) (f : ℕ → ℝ) :
    bitsExpectation (fun _ => p) V (fun S => f S.card) =
      ∑ k ∈ range (V.card + 1),
        (V.card.choose k : ℝ) * p ^ k * (1 - p) ^ (V.card - k) * f k := by
…
```
Mentions: OAI.MatroidProphet.bitsExpectation

theorem OAI.MatroidProphet.SecretaryBinomialMixture.binomial_uniform_subset_mixture line 56

Source documentation

Complete averaging over the binomial prefix length cancels the uniform fixed-size subset normalizer and recovers the product mask expectation.

theorem binomial_uniform_subset_mixture (p : ℝ) (V : Finset α)
    (f : Finset α → ℝ) :
    (∑ k ∈ range (V.card + 1),
      ((V.card.choose k : ℝ) * p ^ k * (1 - p) ^ (V.card - k)) *
        ((V.card.choose k : ℝ)⁻¹ * ∑ S ∈ V.powersetCard k, f S)) =
      bitsExpectation (fun _ => p) V f := by
…

Mentions: OAI.MatroidProphet.bitsExpectation

theorem OAI.MatroidProphet.SecretaryBinomialMixture.predrawn_card_uniform_subset line 84
Source documentation
Equivalent implementation: predraw a product mask, keep only its cardinality, then draw a uniform subset of that cardinality independently.
```
theorem predrawn_card_uniform_subset (p : ℝ) (V : Finset α)
    (f : Finset α → ℝ) :
    bitsExpectation (fun _ => p) V
      (fun B => (V.card.choose B.card : ℝ)⁻¹ *
        ∑ S ∈ V.powersetCard B.card, f S) =
      bitsExpectation (fun _ => p) V f := by
…
```
Mentions: OAI.MatroidProphet.bitsExpectation

theorem OAI.MatroidProphet.SecretaryBinomialMixture.integral_binomial line 98

Source documentation

The finite binomial law used for the initial prefix-length draw, with its actual integral rather than an unnormalized formal sum.

theorem integral_binomial (p : ℝ≥0) (hp : p ≤ 1) (n : ℕ) (f : ℕ → ℝ) :
    (∫ k, f k ∂ProbabilityTheory.binomial n
      ⟨p, p.coe_nonneg, by exact_mod_cast hp⟩) =
      ∑ k ∈ range (n + 1),
        (n.choose k : ℝ) * (p : ℝ) ^ k * (1 - (p : ℝ)) ^ (n - k) * f k := by
…

theorem OAI.MatroidProphet.SecretaryBinomialMixture.integral_binomial_uniform_subset line 109

Source documentation

Sampling the finite binomial length and then a uniform fixed-cardinality subset gives the homogeneous Bernoulli product mask exactly.

theorem integral_binomial_uniform_subset (p : ℝ≥0) (hp : p ≤ 1)
    (V : Finset α) (f : Finset α → ℝ) :
    (∫ k, (V.card.choose k : ℝ)⁻¹ * ∑ S ∈ V.powersetCard k, f S
      ∂ProbabilityTheory.binomial V.card ⟨p, p.coe_nonneg, by exact_mod_cast hp⟩) =
      bitsExpectation (fun _ => (p : ℝ)) V f := by
…

Mentions: OAI.MatroidProphet.bitsExpectation

theorem OAI.MatroidProphet.SecretaryBinomialMixture.integral_uniform_fintype line 119

Source documentation

Conversion from the actual finite uniform law to a normalized sum.

theorem integral_uniform_fintype {β : Type*} [Fintype β] [Nonempty β]
    [MeasurableSpace β] [MeasurableSingletonClass β] (f : β → ℝ) :
    (∫ b, f b ∂(PMF.uniformOfFintype β).toMeasure) =
      (Fintype.card β : ℝ)⁻¹ * ∑ b, f b := by
…