Factored forms of the actual refresh distributions #
The common transcript fixes every refresh seed. These identities retain both latent states during observation, then form the actual refresh by a deterministic map. They make the refreshed source right-only without an independence assumption about the refreshed source and retained right state.
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadFirstRefreshWeight_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)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z) (b : B), 0 ≤ r z b)
:
lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R = mapWeight (fun (p : (LookAheadBaseTranscript Z Q Mid × B) × A) => ((p.1.1, p.2), R (y p.1.1.1.1 p.1.2) 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.lookAheadFirstRefreshWeight_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)
(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))
(lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R) = 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) t.2.1.1
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadTamperedRefresh_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)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
mapWeight
(fun (p : (Z × B) × A) =>
have zq := (p.1.1, q p.1.1 p.1.2, q' p.1.1 p.1.2);
have messages := lookAheadBaseMessage x x' initialSeed W QExt zq p.2;
((((zq, messages), R (y' p.1.1 p.1.2) messages.2.1), p.1.2), p.2))
(factoredWeight w l r) = factoredWeight
(observedTranscriptWeight (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) t.2.2.1)
(fun (tu : LookAheadBaseTranscript Z Q Mid × Out) => lookAheadBaseLeft l x x' initialSeed W QExt tu.1)
(observedTranscriptKernel (lookAheadBaseRight r q q') fun (t : LookAheadBaseTranscript Z Q Mid) (b : B) =>
R (y' t.1.1 b) t.2.2.1)
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadTamperedRefreshWeight_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]
[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 y' : Z → B → Y)
(R : Y → Mid → Out)
(hl : ∀ (z : Z) (a : A), 0 ≤ l z a)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R = mapWeight
(fun (p : ((LookAheadBaseTranscript Z Q Mid × Out) × B) × A) =>
((p.1.1, p.2), R (y p.1.1.1.1.1 p.1.2) p.1.1.1.2.1.2))
(factoredWeight
(observedTranscriptWeight (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) t.2.2.1)
(fun (tu : LookAheadBaseTranscript Z Q Mid × Out) => lookAheadBaseLeft l x x' initialSeed W QExt tu.1)
(observedTranscriptKernel (lookAheadBaseRight r q q') fun (t : LookAheadBaseTranscript Z Q Mid) (b : B) =>
R (y' t.1.1 b) t.2.2.1))