PhysicalPartialSequence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Sequencing finite prefixes that can stop at a live configuration

A called prefix may have reached the continuation, or may still be inside its first program. The construction stops exactly at that interface.

lemma OAI.ContingencyTables.PhysicalPartialSequence.mean_const line 17
lemma OAI.ContingencyTables.PhysicalPartialSequence.halted_all line 23
lemma OAI.ContingencyTables.PhysicalPartialSequence.early_all_eq line 41

theorem OAI.ContingencyTables.PhysicalPartialSequence.left_prefix line 50

Source documentation

Relabelling a physical prefix for sequential composition may shorten its post-halt padding, and preserves the law of its endpoint configuration.

theorem left_prefix (M : Table Γ Q) (N : Table Γ R) (r₀ : R)
    (out : A → Cfg Γ Q) (c : Cfg Γ Q) (p : Experiment A)
    (h : Implements M out c p) :
    ∃ q : Experiment (Cfg Γ Q),
      Implements (seq M N r₀) (leftCfg r₀) (leftCfg r₀ c) q ∧
      (∀ f,q.mean f=p.mean (fun a => f (out a))) ∧ q.cost≤p.cost := by
…

Mentions: OAI.ContingencyTables.Table

theorem OAI.ContingencyTables.PhysicalPartialSequence.left_prefix_injective line 100

Source documentation

When endpoint configurations identify their labels, sequential composition also preserves the complete label law, not just the endpoint law.

theorem left_prefix_injective [Nonempty A] (M : Table Γ Q) (N : Table Γ R) (r₀ : R)
    (out : A → Cfg Γ Q) (hinj : Function.Injective out) (c : Cfg Γ Q) (p : Experiment A)
    (h : Implements M out c p) :
    ∃ q : Experiment A,
      Implements (seq M N r₀) (fun a => leftCfg r₀ (out a)) (leftCfg r₀ c) q ∧
      (∀ f,q.mean f=p.mean f) ∧ q.cost≤p.cost := by
…

Mentions: OAI.ContingencyTables.Table