Coupling.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Initial-seed / random-prefix coupling

The complete table is drawn with the initial seed, before the independent arrival permutation. Reassociation here is only a proof of the joint law; the implementation does not defer any table randomness until after the prefix.

theorem OAI.MatroidProphet.Secretary.initial_seed_reassociate line 31

Source documentation

Moving the independent arrival randomness next to the source seed does not change the product law; the entire precommitted table remains present.

theorem initial_seed_reassociate (μ : Measure U) (ν : Measure T) (η : Measure S)
    [SFinite μ] [SFinite ν] [SFinite η] :
    MeasurePreserving (fun z : (U × T) × S => ((z.1.1, z.2), z.1.2))
      ((μ.prod ν).prod η) ((μ.prod η).prod ν) := by
…

theorem OAI.MatroidProphet.Secretary.observation_table_joint line 43

Source documentation

Any observation of source seed and independent prefix randomness retains independence from the complete pre-drawn table.

theorem observation_table_joint (μ : Measure U) (ν : Measure T) (η : Measure S)
    (ρ : Measure B) [SFinite μ] [SFinite ν] [SFinite η]
    (index : U × S → B) (hi : Measurable index)
    (hindex : (μ.prod η).map index = ρ) :
    ((μ.prod ν).prod η).map
      (fun z : (U × T) × S => (index (z.1.1, z.2), z.1.2)) = ρ.prod ν := by
…

theorem OAI.MatroidProphet.Secretary.reconstructed_seed_law line 56

Source documentation

Decoding the precommitted table after observing the prefix has the same law as selecting from an independent table at an index with the required observation law. No future arrival information is an input to decode.

theorem reconstructed_seed_law (μ : Measure U) (ν : Measure T) (η : Measure S)
    (ρ : Measure B) (ξ : Measure A) [SFinite μ] [SFinite ν] [SFinite η]
    (index : U × S → B) (hi : Measurable index)
    (hindex : (μ.prod η).map index = ρ)
    (decode : B × T → A) (hd : Measurable decode)
    (hdecode : (ρ.prod ν).map decode = ξ) :
    ((μ.prod ν).prod η).map
      (fun z : (U × T) × S => decode (index (z.1.1, z.2), z.1.2)) = ξ := by
…

def OAI.MatroidProphet.Secretary.conditionalSourceLaw line 82
Source documentation
Normalize the actual source measure on each observation fiber.
```
noncomputable def conditionalSourceLaw (μ : Measure A) (obs : A → B)
    (fallback : A) (b : B) : Measure A :=
…
```
instance OAI.MatroidProphet.Secretary.conditionalSourceLaw_probability line 89

theorem OAI.MatroidProphet.Secretary.observation_graph_atom line 96

Source documentation

The graph of the observation keeps the full source realization.

theorem observation_graph_atom (μ : Measure A) (obs : A → B) (b : B) (a : A) :
    (μ.map (fun a => (obs a, a))) {(b, a)} =
      if obs a = b then μ {a} else 0 := by
…

theorem OAI.MatroidProphet.Secretary.conditionalSourceLaw_joint_atom line 122
Source documentation
The true observation marginal times the normalized conditional law is the exact graph law of the complete source seed, including unused coordinates.
```
theorem conditionalSourceLaw_joint_atom (μ : Measure A) [IsProbabilityMeasure μ]
    (obs : A → B) (fallback : A) (b : B) (a : A) :
    (μ.map obs) {b} * conditionalSourceLaw μ obs fallback b {a} =
      (μ.map (fun a => (obs a, a))) {(b, a)} := by
…
```
Mentions: OAI.MatroidProphet.Secretary.conditionalSourceLaw

theorem OAI.MatroidProphet.Secretary.conditional_table_joint line 147

Source documentation

Predrawing every conditional source seed and selecting the observed fiber reconstructs the complete source joint law exactly.

theorem conditional_table_joint (μ : Measure A) [IsProbabilityMeasure μ]
    (obs : A → B) (fallback : A) :
    ((μ.map obs).prod (Measure.pi (conditionalSourceLaw μ obs fallback))).map
      (fun z : B × (B → A) => (z.1, z.2 z.1)) =
      μ.map (fun a => (obs a, a)) := by
…

Mentions: OAI.MatroidProphet.Secretary.conditionalSourceLaw

theorem OAI.MatroidProphet.Secretary.precommitted_source_joint line 159

Source documentation

The actual initial seed is (source seed, whole conditional table), independent of prefix randomness. If the prefix observation has the true observation law, lookup recovers the full joint source law.

theorem precommitted_source_joint {S : Type*} [MeasurableSpace S]
    (μ : Measure A) [IsProbabilityMeasure μ] (η : Measure S) [SFinite η]
    (obs : A → B) (fallback : A) (index : A × S → B)
    (hi : Measurable index) (hindex : (μ.prod η).map index = μ.map obs) :
    ((μ.prod (Measure.pi (conditionalSourceLaw μ obs fallback))).prod η).map
      (fun z : (A × (B → A)) × S =>
        (index (z.1.1, z.2), z.1.2 (index (z.1.1, z.2)))) =
      μ.map (fun a => (obs a, a)) := by
…

Mentions: OAI.MatroidProphet.Secretary.conditionalSourceLaw

theorem OAI.MatroidProphet.Secretary.precommitted_source_marginal line 174

Source documentation

In particular the reconstructed seed, with all unused coordinates, has the original source marginal.

theorem precommitted_source_marginal {S : Type*} [MeasurableSpace S]
    (μ : Measure A) [IsProbabilityMeasure μ] (η : Measure S) [SFinite η]
    (obs : A → B) (fallback : A) (index : A × S → B)
    (hi : Measurable index) (hindex : (μ.prod η).map index = μ.map obs) :
    ((μ.prod (Measure.pi (conditionalSourceLaw μ obs fallback))).prod η).map
      (fun z : (A × (B → A)) × S => z.1.2 (index (z.1.1, z.2))) = μ := by
…

Mentions: OAI.MatroidProphet.Secretary.conditionalSourceLaw

theorem OAI.MatroidProphet.Secretary.ae_precommitted_source_observation line 192
abbrev OAI.MatroidProphet.Secretary.SourceObservation line 216
abbrev OAI.MatroidProphet.Secretary.CouplingSeed line 219
Source documentation
The full source seed together with every conditional draw, all predrawn.
```
abbrev CouplingSeed (n : ℕ) :=
…
```
def OAI.MatroidProphet.Secretary.couplingObservation line 222
def OAI.MatroidProphet.Secretary.couplingKernel line 226
instance OAI.MatroidProphet.Secretary.couplingKernel_probability line 230
def OAI.MatroidProphet.Secretary.couplingSeedLaw line 237
Source documentation
This initial seed law depends on the matroid but not on any weights.
```
noncomputable def couplingSeedLaw {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) : Measure (CouplingSeed n) :=
…
```
Mentions: OAI.MatroidProphet.Secretary.CouplingSeed
instance OAI.MatroidProphet.Secretary.couplingSeedLaw_probability line 241
def OAI.MatroidProphet.Secretary.couplingLength line 247
Source documentation
The cutoff is fixed before arrivals using only the first part of the seed.
```
noncomputable def couplingLength {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (q : CouplingSeed n) : Fin (n + 1) :=
…
```
Mentions: OAI.MatroidProphet.Secretary.CouplingSeed
def OAI.MatroidProphet.Secretary.couplingDecode line 255
Source documentation
Lookup needs only the seed and the observed label set, not its weights or the future suffix order.
```
def couplingDecode {n : ℕ} (q : CouplingSeed n) (P : Finset (Fin n)) :
    Seed (mainSeedBits n) := q.2 (mainBranch q.1, P)
```
Mentions: OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.mainBranch
def OAI.MatroidProphet.Secretary.couplingIndex line 258
theorem OAI.MatroidProphet.Secretary.coupling_joint_of_prefix_law line 265
Source documentation
The remaining input is the independently proved random-prefix law, not a hypothesis of the final secretary endpoint.
```
theorem coupling_joint_of_prefix_law {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ)
    (hprefix : ((sourceSeedLaw n).prod (uniformArrivalLaw n)).map (couplingIndex M hE) =
      (sourceSeedLaw n).map (couplingObservation M hE)) :
    ((couplingSeedLaw M hE).prod (uniformArrivalLaw n)).map
      (fun z : CouplingSeed n × ArrivalOrder n =>
        ((mainBranch z.1.1, orderPrefix z.2 (couplingLength M hE z.1).val),
          couplingDecode z.1 (orderPrefix z.2 (couplingLength M hE z.1).val))) =
      (sourceSeedLaw n).map (fun r => (couplingObservation M hE r, r)) := by
…
```
Mentions: OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.Secretary.uniformArrivalLaw, OAI.MatroidProphet.Secretary.couplingIndex, OAI.MatroidProphet.Secretary.couplingObservation, OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.Secretary.couplingLength, OAI.MatroidProphet.Secretary.couplingDecode
theorem OAI.MatroidProphet.Secretary.coupling_marginal_of_prefix_law line 278
theorem OAI.MatroidProphet.Secretary.coupling_mask_ae_of_prefix_law line 290
theorem OAI.MatroidProphet.Secretary.coupling_source_prefix_law line 311
Source documentation
Concrete random-prefix identity, with no transport premise.
```
theorem coupling_source_prefix_law {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) :
    ((sourceSeedLaw n).prod (uniformArrivalLaw n)).map (couplingIndex M hE) =
      (sourceSeedLaw n).map (couplingObservation M hE) := by
…
```
Mentions: OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.Secretary.uniformArrivalLaw, OAI.MatroidProphet.Secretary.couplingIndex, OAI.MatroidProphet.Secretary.couplingObservation
theorem OAI.MatroidProphet.Secretary.coupling_joint_law line 319
Source documentation
The complete initial finite seed and independent arrival order reconstruct exactly the original full source graph law. No assumption is added to an endpoint.
```
theorem coupling_joint_law {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) :
    ((couplingSeedLaw M hE).prod (uniformArrivalLaw n)).map
      (fun z : CouplingSeed n × ArrivalOrder n =>
        ((mainBranch z.1.1, orderPrefix z.2 (couplingLength M hE z.1).val),
          couplingDecode z.1 (orderPrefix z.2 (couplingLength M hE z.1).val))) =
      (sourceSeedLaw n).map (fun r => (couplingObservation M hE r, r)) :=
…
```
Mentions: OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.Secretary.uniformArrivalLaw, OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.Secretary.couplingLength, OAI.MatroidProphet.Secretary.couplingDecode, OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.Secretary.couplingObservation
theorem OAI.MatroidProphet.Secretary.coupling_source_law line 329
Source documentation
The decoded seed retains the law of every source bit, including unused bits.
```
theorem coupling_source_law {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) :
    ((couplingSeedLaw M hE).prod (uniformArrivalLaw n)).map
      (fun z : CouplingSeed n × ArrivalOrder n =>
        couplingDecode z.1 (orderPrefix z.2 (couplingLength M hE z.1).val)) =
      sourceSeedLaw n :=
…
```
Mentions: OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.Secretary.uniformArrivalLaw, OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.Secretary.couplingDecode, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.Secretary.couplingLength, OAI.MatroidProphet.sourceSeedLaw
theorem OAI.MatroidProphet.Secretary.coupling_mask_ae line 339
Source documentation
Almost-sure mask agreement for the concrete initial-seed experiment. Every-seed feasibility separately uses the replay's mismatch-rejection guard.
```
theorem coupling_mask_ae {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) :
    ∀ᵐ z : CouplingSeed n × ArrivalOrder n
      ∂(couplingSeedLaw M hE).prod (uniformArrivalLaw n),
      (completeHiddenRule M hE).mask
          (couplingDecode z.1 (orderPrefix z.2 (couplingLength M hE z.1).val)) =
        orderPrefix z.2 (couplingLength M hE z.1).val :=
…
```
Mentions: OAI.MatroidProphet.Secretary.CouplingSeed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.Secretary.couplingSeedLaw, OAI.MatroidProphet.Secretary.uniformArrivalLaw, OAI.MatroidProphet.completeHiddenRule, OAI.MatroidProphet.Secretary.couplingDecode, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.Secretary.couplingLength