Joint-mass envelopes under finite two-sided observations #
Refining a left event cannot increase its joint source mass. Averaging over the right observation preserves the total envelope, while an additional finite leak multiplies that total by its alphabet size. No conditional entropy hypothesis is imposed on an individual transcript fiber.
noncomputable def
Algebraic.Cutwidth.Extractor.Internal.mergingEnvelope
{Z : Type u_1}
{B : Type u_3}
{U : Type u_5}
{V : Type u_6}
{W : Type u_7}
[Fintype B]
(r : Z → B → ℝ)
(v : Z → B → V)
(μ : Z × U → ℝ)
(t : (Z × V) × U × W)
:
The refined joint envelope weights each old row by its right observation probability.
Equations
- Algebraic.Cutwidth.Extractor.Internal.mergingEnvelope r v μ t = Algebraic.Cutwidth.Extractor.mapWeight (v t.1.1) (r t.1.1) t.1.2 * μ (t.1.1, t.2.1)
Instances For
theorem
Algebraic.Cutwidth.Extractor.Internal.mergingEnvelope_nonnegative
{Z : Type u_1}
{B : Type u_3}
{U : Type u_5}
{V : Type u_6}
{W : Type u_7}
[Fintype B]
[Fintype V]
(r : Z → B → ℝ)
(v : Z → B → V)
(μ : Z × U → ℝ)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(hμ : ∀ (t : Z × U), 0 ≤ μ t)
(t : (Z × V) × U × W)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.leakageSourceWeight_cap
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{U : Type u_5}
{V : Type u_6}
{W : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype V]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(u : Z → A → U)
(v : Z → B → V)
(leak : Z → V → A → W)
(μ : Z × U → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(cap : ∀ (z : Z) (u₀ : U) (x₀ : X), w z * mapWeight (fun (a : A) => (u z a, x z a)) (l z) (u₀, x₀) ≤ μ (z, u₀))
(t : (Z × V) × U × W)
(x₀ : X)
: