Precommit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Predrawing every conditional seed

A finite table of independent conditional seeds can be sampled before the observation prefix. Looking up the entry indexed by the observed prefix uses no later randomness. The whole table, including unused entries, may be disclosed. These lemmas are probability identities only; an actual prefix law and an actual history-only online replay remain separate obligations.

theorem OAI.MatroidProphet.SecretaryPrecommit.table_eval_map line 30

Source documentation

Every precommitted coordinate retains its specified conditional law.

theorem table_eval_map (κ : B → Measure A) [∀ b, IsProbabilityMeasure (κ b)]
    (b : B) :
    (Measure.pi κ).map (fun t : B → A => t b) = κ b :=
…

theorem OAI.MatroidProphet.SecretaryPrecommit.selected_joint_singleton line 37

Source documentation

Exact joint atoms of the observed index and the selected precommitted seed. The index law is independent of the entire table, not merely its selected entry.

theorem selected_joint_singleton (ρ : Measure B) (κ : B → Measure A)
    [∀ b, IsProbabilityMeasure (κ b)] (b : B) (a : A) :
    ((ρ.prod (Measure.pi κ)).map
      (fun z : B × (B → A) => (z.1, z.2 z.1))) {(b, a)} =
        ρ {b} * κ b {a} := by
…

theorem OAI.MatroidProphet.SecretaryPrecommit.selected_joint_eq line 60

Source documentation

A target joint law is recovered from its conditional-fiber factorization.

theorem selected_joint_eq (ρ : Measure B) (κ : B → Measure A)
    [∀ b, IsProbabilityMeasure (κ b)] (ν : Measure (B × A))
    (hν : ∀ b a, ν {(b, a)} = ρ {b} * κ b {a}) :
    (ρ.prod (Measure.pi κ)).map
      (fun z : B × (B → A) => (z.1, z.2 z.1)) = ν := by
…

theorem OAI.MatroidProphet.SecretaryPrecommit.integral_selected line 70

Source documentation

Integrating after table lookup gives precisely the conditional mixture.

theorem integral_selected (ρ : Measure B) [IsFiniteMeasure ρ]
    (κ : B → Measure A) [∀ b, IsProbabilityMeasure (κ b)]
    (f : B → A → ℝ) :
    (∫ z : B × (B → A), f z.1 (z.2 z.1) ∂ρ.prod (Measure.pi κ)) =
      ∫ b, ∫ a, f b a ∂κ b ∂ρ := by
…

theorem OAI.MatroidProphet.SecretaryPrecommit.ae_table_fibers line 87
Source documentation
Every table coordinate satisfies its fiber constraint almost surely, simultaneously, so an arbitrary later lookup cannot choose a bad coordinate.
```
theorem ae_table_fibers (κ : B → Measure A) [∀ b, IsProbabilityMeasure (κ b)]
    (G : B → A → Prop) (hG : ∀ b, ∀ᵐ a ∂κ b, G b a) :
    ∀ᵐ t : B → A ∂Measure.pi κ, ∀ b, G b (t b) := by
…
```

theorem OAI.MatroidProphet.SecretaryPrecommit.selected_joint_of_map line 96

Source documentation

The observed index may be a function of a larger random-prefix experiment. Only independence of that experiment from the entire precommitted table is used.

theorem selected_joint_of_map {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [SFinite μ] (ρ : Measure B)
    (P : Ω → B) (hP : Measurable P) (hmap : μ.map P = ρ)
    (κ : B → Measure A) [∀ b, IsProbabilityMeasure (κ b)] :
    (μ.prod (Measure.pi κ)).map
      (fun z : Ω × (B → A) => (P z.1, z.2 (P z.1))) =
    (ρ.prod (Measure.pi κ)).map
      (fun z : B × (B → A) => (z.1, z.2 z.1)) := by
…