Actual selected-refresh identities #
The second-output law is the existing tampered-refresh law with its extra right output discarded. Both choices have the same exact common transcript factorization and refresh the original right source with a fixed seed.
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadSelectedRefreshWeight_false
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(y : Z → B → Y)
(R : Y → Mid → Out)
:
lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R false = lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadSelectedRefreshWeight_true_eq_map
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
[Fintype Mid]
[Fintype Out]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(y : Z → B → Y)
(R : Y → Mid → Out)
:
lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R true = mapWeight (fun (p : ((LookAheadBaseTranscript Z Q Mid × Out) × A) × Out) => ((p.1.1.1, p.1.2), p.2))
(lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y R)
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadSelectedRefreshWeight_probability
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
[Fintype Mid]
[Fintype Out]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(y : Z → B → Y)
(R : Y → Mid → Out)
(second : Bool)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R second)
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadSelectedRefreshWeight_eq_factored
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
[Fintype Mid]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(y : Z → B → Y)
(R : Y → Mid → Out)
(second : Bool)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
:
lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R second = mapWeight
(fun (p : (LookAheadBaseTranscript Z Q Mid × B) × A) =>
((p.1.1, p.2), R (y p.1.1.1.1 p.1.2) (if second = true then p.1.1.2.1.2 else p.1.1.2.1.1)))
(factoredWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt)
(lookAheadBaseLeft l x x' initialSeed W QExt) (lookAheadBaseRight r q q'))
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadSelectedRefreshWeight_retainedSeed
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
[Fintype Mid]
[Fintype Out]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(y : Z → B → Y)
(R : Y → Mid → Out)
(second : Bool)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
:
mapWeight (fun (p : (LookAheadBaseTranscript Z Q Mid × A) × Out) => (p.1.1, p.2))
(lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R second) = retainedSeedWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt) (lookAheadBaseRight r q q')
fun (t : LookAheadBaseTranscript Z Q Mid) (b : B) => R (y t.1.1 b) (if second = true then t.2.1.2 else t.2.1.1)