PrecommittedKernel.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Precommitted finite conditional-kernel tables

The secretary reconstruction may be implemented with no randomness drawn after arrivals: draw one independent kernel output for every possible finite observation before arrivals, and later read only the entry indexed by the observation. The entire table, including unused entries, is part of the initial seed.

These lemmas establish the law of that concrete construction. They do not assert independence after conditioning on the entire table, and do not assume a secretary transport theorem or a reward guarantee.

theorem OAI.MatroidProphet.PrecommittedKernel.map_eval line 31

Source documentation

Reading one fixed coordinate from the initial table has the prescribed law.

theorem map_eval (κ : I → Measure A) [∀ i, IsProbabilityMeasure (κ i)] (i : I) :
    Measure.map (fun q : I → A => q i) (Measure.pi κ) = κ i :=
…

theorem OAI.MatroidProphet.PrecommittedKernel.integral_eval line 38
Source documentation
Every statistic of one kernel output has the same expectation under the precommitted table construction. No later draw is needed.
```
theorem integral_eval (κ : I → Measure A) [∀ i, IsProbabilityMeasure (κ i)]
    (i : I) (f : A → ℝ) :
    (∫ q : I → A, f (q i) ∂Measure.pi κ) = ∫ a, f a ∂κ i := by
…
```

theorem OAI.MatroidProphet.PrecommittedKernel.integral_joint line 48

Source documentation

An observation independent of the whole initial table selects exactly its conditional kernel. The function may depend jointly on observation and output.

theorem integral_joint (μ : Measure I) [IsFiniteMeasure μ]
    (κ : I → Measure A) [∀ i, IsProbabilityMeasure (κ i)] (f : I → A → ℝ) :
    (∫ z : I × (I → A), f z.1 (z.2 z.1) ∂μ.prod (Measure.pi κ)) =
      ∫ i, ∫ a, f i a ∂κ i ∂μ := by
…

theorem OAI.MatroidProphet.PrecommittedKernel.joint_singleton line 58

Source documentation

Exact joint atom law, retaining the observation as well as reconstructed output. This is stronger than only identifying the output marginal.

theorem joint_singleton (μ : Measure I) [IsFiniteMeasure μ]
    (κ : I → Measure A) [∀ i, IsProbabilityMeasure (κ i)] (i : I) (a : A) :
    Measure.map (fun z : I × (I → A) => (z.1, z.2 z.1))
      (μ.prod (Measure.pi κ)) {(i, a)} = μ {i} * κ i {a} := by
…

theorem OAI.MatroidProphet.PrecommittedKernel.map_joint_eq line 82

Source documentation

A candidate joint law is recovered exactly if its atoms have the specified observation marginal times conditional kernel law. All unused table coordinates remain present in the concrete initial probability space.

theorem map_joint_eq (μ : Measure I) [IsFiniteMeasure μ]
    (κ : I → Measure A) [∀ i, IsProbabilityMeasure (κ i)] (ν : Measure (I × A))
    (hν : ∀ i a, ν {(i, a)} = μ {i} * κ i {a}) :
    Measure.map (fun z : I × (I → A) => (z.1, z.2 z.1))
      (μ.prod (Measure.pi κ)) = ν := by
…

theorem OAI.MatroidProphet.PrecommittedKernel.map_random_index line 94

Source documentation

The observation may itself be any measurable function of a separate random experiment (for example a binomial cutoff and uniform arrival permutation). Only its marginal law matters to the precommitted-table reconstruction.

theorem map_random_index {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [SFinite μ] (X : Ω → I) (hX : Measurable X)
    (κ : I → Measure A) [∀ i, IsProbabilityMeasure (κ i)] :
    Measure.map (fun z : Ω × (I → A) => (X z.1, z.2 (X z.1)))
      (μ.prod (Measure.pi κ)) =
    Measure.map (fun z : I × (I → A) => (z.1, z.2 z.1))
      ((Measure.map X μ).prod (Measure.pi κ)) := by
…

theorem OAI.MatroidProphet.PrecommittedKernel.integral_eval_dependent line 115
Source documentation
Dependent kernel tables allow the output type at each observation to be its valid fiber. Thus every initial table, including null-probability tables, obeys the reconstruction constraint by type, rather than only almost surely.
```
theorem integral_eval_dependent (κ : (i : I) → Measure (B i))
    [∀ i, IsProbabilityMeasure (κ i)] (i : I) (f : B i → ℝ) :
    (∫ q : (i : I) → B i, f (q i) ∂Measure.pi κ) = ∫ a, f a ∂κ i := by
…
```

theorem OAI.MatroidProphet.PrecommittedKernel.integral_joint_dependent line 124

Source documentation

Exact conditional expectation for dependent-fiber precommitted tables.

theorem integral_joint_dependent (μ : Measure I) [IsFiniteMeasure μ]
    (κ : (i : I) → Measure (B i)) [∀ i, IsProbabilityMeasure (κ i)]
    (f : (i : I) → B i → ℝ) :
    (∫ z : I × ((i : I) → B i), f z.1 (z.2 z.1) ∂μ.prod (Measure.pi κ)) =
      ∫ i, ∫ a, f i a ∂κ i ∂μ := by
…