CutoffLaw.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual initial branch/cutoff law

For the complete precommitted coupling seed, the initial branch and cutoff have exactly the fair-branch/Binomial joint law in secretary.tex lines 54--66. This averages the entire conditional table; it is not conditioning on the complete Q. The cutoff is chosen before weights or arrival randomness. Empty/full cutoffs and the empty ground set are included without exclusions.

theorem OAI.MatroidProphet.Secretary.integral_couplingSeedLaw_fst line 23
Source documentation
A statistic of the initial source component is unaffected by predrawing the entire independent conditional table. No table entry is hidden or removed.
```
theorem integral_couplingSeedLaw_fst {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (f : Seed (mainSeedBits n) → ℝ) :
    (∫ q : CouplingSeed n, f q.1 ∂couplingSeedLaw M hE) =
      ∫ r, f r ∂sourceSeedLaw n := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.sourceSeedLaw
theorem OAI.MatroidProphet.Secretary.integral_initial_branch_cutoff line 32
Source documentation
Exact branchwise Binomial law of the actual initial cutoff, not of a reconstructed seed or a post-observation conditional full-Q distribution.
```
theorem integral_initial_branch_cutoff {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (j : Bool) (f : ℕ → ℝ) :
    (∫ q : CouplingSeed n,
      (if mainBranch q.1 = j then f (couplingLength M hE q).val else 0)
      ∂couplingSeedLaw M hE) =
      (1 / 2 : ℝ) * ∑ k ∈ range (n + 1),
        (n.choose k : ℝ) * (branchRate j) ^ k *
          (1 - branchRate j) ^ (n - k) * f k := by
…
```
Mentions: OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.Secretary.couplingLength, OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.Secretary.branchRate
theorem OAI.MatroidProphet.Secretary.integral_initial_branch_cutoff_binomial line 52
Source documentation
The same actual-Q identity with the library Binomial probability measure.
```
theorem integral_initial_branch_cutoff_binomial {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (j : Bool) (f : ℕ → ℝ) :
    (∫ q : CouplingSeed n,
      (if mainBranch q.1 = j then f (couplingLength M hE q).val else 0)
      ∂couplingSeedLaw M hE) =
      (1 / 2 : ℝ) * ∫ k,
        f k ∂ProbabilityTheory.binomial n
          ⟨branchRate j, (branchRate_pos j).le, (branchRate_lt_one j).le⟩ := by
…
```
Mentions: OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.Secretary.couplingLength, OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.Secretary.branchRate, OAI.MatroidProphet.Secretary.branchRate_pos, OAI.MatroidProphet.Secretary.branchRate_lt_one

theorem OAI.MatroidProphet.Secretary.initial_branch_cutoff_atom_real line 64

Source documentation

Real joint atoms of the actual initial branch and bounded cutoff.

theorem initial_branch_cutoff_atom_real {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (j : Bool) (k : Fin (n + 1)) :
    (couplingSeedLaw M hE).real
      {q | mainBranch q.1 = j ∧ (couplingLength M hE q).val = k.val} =
      (1 / 2 : ℝ) * ((n.choose k.val : ℝ) * (branchRate j) ^ k.val *
        (1 - branchRate j) ^ (n - k.val)) := by
…

Mentions: OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.Secretary.couplingLength, OAI.MatroidProphet.Secretary.branchRate

theorem OAI.MatroidProphet.Secretary.initial_branch_cutoff_atom line 78

Source documentation

The probability-measure version, retaining the branch factor one half.

theorem initial_branch_cutoff_atom {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (j : Bool) (k : Fin (n + 1)) :
    couplingSeedLaw M hE
      {q | mainBranch q.1 = j ∧ (couplingLength M hE q).val = k.val} =
      ENNReal.ofReal ((1 / 2 : ℝ) * ((n.choose k.val : ℝ) *
        (branchRate j) ^ k.val * (1 - branchRate j) ^ (n - k.val))) := by
…

Mentions: OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.Secretary.couplingLength, OAI.MatroidProphet.Secretary.branchRate