BernoulliConditionalFiber.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact conditional fibers of a finite Bernoulli product law

A fixed outside mask is a genuine conditioning event. Restricting the full product-law expectation to that event factors into its atom probability times the expectation over the unrevealed coordinates. The unnormalized identity also covers zero-probability fibers and endpoint Bernoulli rates.

lemma OAI.MatroidProphet.bitsExpectation_mask_atom line 19
Source documentation
The weighted expectation of a single supported mask atom.
```
lemma bitsExpectation_mask_atom (q : α → ℝ) (V A : Finset α)
    (hA : A ⊆ V) (c : ℝ) :
    bitsExpectation q V (fun S => if S = A then c else 0) =
      bitsWeight q V A * c := by
…
```
Mentions: OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.bitsWeight

theorem OAI.MatroidProphet.bitsExpectation_fixed_outside_event line 27

Source documentation

Restrict a full product-law expectation to one outside-coordinate fiber. There are no positivity assumptions: null fibers are handled exactly.

theorem bitsExpectation_fixed_outside_event (q : α → ℝ)
    (V G A : Finset α) (hG : G ⊆ V) (hA : A ⊆ V \ G)
    (f : Finset α → ℝ) :
    bitsExpectation q V (fun T => if T \ G = A then f T else 0) =
      bitsWeight q (V \ G) A *
        bitsExpectation q G (fun B => f (A ∪ B)) := by
…

Mentions: OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.bitsWeight

theorem OAI.MatroidProphet.bitsExpectation_fixed_outside_probability line 67
Source documentation
The probability of a specified outside mask is exactly its product atom.
```
theorem bitsExpectation_fixed_outside_probability (q : α → ℝ)
    (V G A : Finset α) (hG : G ⊆ V) (hA : A ⊆ V \ G) :
    bitsExpectation q V (fun T => if T \ G = A then 1 else 0) =
      bitsWeight q (V \ G) A := by
…
```
Mentions: OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.bitsWeight

theorem OAI.MatroidProphet.bitsExpectation_condition_on_outside line 76

Source documentation

On a nonnull outside fiber, the normalized conditional expectation is exactly the fresh-coordinate expectation used in the accounting contract.

theorem bitsExpectation_condition_on_outside (q : α → ℝ)
    (V G A : Finset α) (hG : G ⊆ V) (hA : A ⊆ V \ G)
    (hpos : bitsWeight q (V \ G) A ≠ 0) (f : Finset α → ℝ) :
    bitsExpectation q V (fun T => if T \ G = A then f T else 0) /
      bitsExpectation q V (fun T => if T \ G = A then 1 else 0) =
    bitsExpectation q G (fun B => f (A ∪ B)) := by
…

Mentions: OAI.MatroidProphet.bitsWeight, OAI.MatroidProphet.bitsExpectation

lemma OAI.MatroidProphet.bitsWeight_pos_of_interior line 88
Source documentation
Interior coordinate rates make every outside atom positive, including empty/full masks and the empty outside ground set.
```
lemma bitsWeight_pos_of_interior (q : α → ℝ) (V A : Finset α)
    (hq0 : ∀ e ∈ V, 0 < q e) (hq1 : ∀ e ∈ V, q e < 1) :
    0 < bitsWeight q V A := by
…
```
Mentions: OAI.MatroidProphet.bitsWeight

theorem OAI.MatroidProphet.bitsExpectation_condition_on_outside_const line 100

Source documentation

Constant interior-rate specialization: no nonnull-fiber premise remains. This applies in particular to the source's t = 2⁻¹⁴⁰.

theorem bitsExpectation_condition_on_outside_const
    (t : ℝ) (ht0 : 0 < t) (ht1 : t < 1)
    (V G A : Finset α) (hG : G ⊆ V) (hA : A ⊆ V \ G)
    (f : Finset α → ℝ) :
    bitsExpectation (fun _ => t) V (fun T => if T \ G = A then f T else 0) /
      bitsExpectation (fun _ => t) V (fun T => if T \ G = A then 1 else 0) =
    bitsExpectation (fun _ => t) G (fun B => f (A ∪ B)) := by
…

Mentions: OAI.MatroidProphet.bitsExpectation