InformationTheory.Shannon.IIDProductInput.Joint
i.i.d. ambient (μ, Xs, Ys) from a joint distribution (rate-distortion variant) #
This file mirrors IIDProductInput/Basic.lean (the channel-coding variant built from a
source pmf p and channel W), but takes a joint distribution
joint : Measure (α × β) directly as input. This is the shape required by the
rate-distortion achievability proof, where the ambient law is specified jointly
rather than as (p ⊗ₘ W).
The coordinate random variables iidXs, iidYs and the joint sequence
jointSequence iidXs iidYs are reused verbatim from
InformationTheory.Shannon.IIDProductInput; only the underlying product measure
differs (Measure.infinitePi (fun _ => joint) instead of
Measure.infinitePi (fun _ => jointDistribution p W)).
Ambient measure on ℕ → α × β #
InformationTheory.Shannon.iidAmbientJointMeasure
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
:
MeasureTheory.Measure (ℕ → α × β)
The i.i.d. ambient measure built from a joint distribution joint:
Measure.infinitePi (fun _ : ℕ => joint) on ℕ → α × β.
Equations
- InformationTheory.Shannon.iidAmbientJointMeasure joint = MeasureTheory.Measure.infinitePi fun (x : ℕ) => joint
Instances For
Used by
InformationTheory.Shannon.iidAmbientJointMeasure.instIsProbabilityMeasure
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
:
Used by
Marginal laws #
InformationTheory.Shannon.iidAmbientJoint_map_jointSequence
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(i : ℕ)
:
The joint sequence marginal at index i is joint itself.
Used by
InformationTheory.Shannon.iidAmbientJoint_map_iidXs
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(i : ℕ)
:
The Xs marginal at index i is joint.map Prod.fst.
Used by
InformationTheory.Shannon.iidAmbientJoint_map_iidYs
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(i : ℕ)
:
The Ys marginal at index i is joint.map Prod.snd.
Used by
IdentDistrib along each axis #
InformationTheory.Shannon.iidAmbientJoint_identDistrib_iidXs
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(i : ℕ)
:
ProbabilityTheory.IdentDistrib (ChannelCoding.iidXs i) (ChannelCoding.iidXs 0) (iidAmbientJointMeasure joint)
(iidAmbientJointMeasure joint)
Used by
InformationTheory.Shannon.iidAmbientJoint_identDistrib_joint
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(i : ℕ)
:
Used by
iIndepFun along each axis #
InformationTheory.Shannon.iidAmbientJoint_iIndepFun_iidXs
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
:
ProbabilityTheory.iIndepFun (fun (i : ℕ) => ChannelCoding.iidXs i) (iidAmbientJointMeasure joint)
Used by
InformationTheory.Shannon.iidAmbientJoint_iIndepFun_joint
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
:
ProbabilityTheory.iIndepFun (fun (i : ℕ) => ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs i)
(iidAmbientJointMeasure joint)
Used by
Positivity of singleton marginals #
InformationTheory.Shannon.iidAmbientJoint_iidXs_real_singleton_pos
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[Nonempty β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(h_joint_pos : ∀ (p : α × β), 0 < joint.real {p})
(x : α)
:
Used by
InformationTheory.Shannon.iidAmbientJoint_iidYs_real_singleton_pos
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass β]
[Nonempty α]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(h_joint_pos : ∀ (p : α × β), 0 < joint.real {p})
(y : β)
:
Used by
InformationTheory.Shannon.iidAmbientJoint_joint_real_singleton_pos
source{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(joint : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure joint]
(h_joint_pos : ∀ (p : α × β), 0 < joint.real {p})
(q : α × β)
: