Functional representation lemma

DefinitionSigma-algebra of the auxiliary coordinate#✓fully proved

For measurable spaces \(X\), \(Y\) and \(S\), this is the sigma-algebra on \((X \times Y) \times S\) generated by the projection \(((x, y), s) \mapsto s\) onto \(S\), regarded as a sub-sigma-algebra of the product sigma-algebra on \((X \times Y) \times S\).

def auxiliaryConditioning {X Y S : Type*}
    [mX : MeasurableSpace X] [mY : MeasurableSpace Y] [mS : MeasurableSpace S] :
    {m : MeasurableSpace ((X × Y) × S) //
      m ≤ @Prod.instMeasurableSpace (X × Y) S (@Prod.instMeasurableSpace X Y mX mY) mS} :=
  ⟨MeasurableSpace.comap Prod.snd mS, measurable_snd.comap_le⟩

Used by 1

Used byConditional entropy of the output given the auxiliary variable

DefinitionSigma-algebra of the input and auxiliary coordinates#✓fully proved

For measurable spaces \(X\), \(Y\) and \(S\), this is the sigma-algebra on \((X \times Y) \times S\) generated by the map \(((x, y), s) \mapsto (x, s)\) into \(X \times S\) with its product sigma-algebra, regarded as a sub-sigma-algebra of the product sigma-algebra on \((X \times Y) \times S\).

def inputAuxiliaryConditioning {X Y S : Type*}
    [mX : MeasurableSpace X] [mY : MeasurableSpace Y] [mS : MeasurableSpace S] :
    {m : MeasurableSpace ((X × Y) × S) //
      m ≤ @Prod.instMeasurableSpace (X × Y) S (@Prod.instMeasurableSpace X Y mX mY) mS} :=
  ⟨MeasurableSpace.comap (fun z => (z.1.1, z.2)) (@Prod.instMeasurableSpace X S mX mS),
    (measurable_fst.fst.prodMk measurable_snd).comap_le⟩

Used by 1

Used byConditional entropy of the output given input and auxiliary variable

DefinitionConditional entropy of the output given the auxiliary variable#✓fully proved

For a probability measure \(\nu\) on \((X \times Y) \times S\), \(H(Y \mid S)\) is the conditional Shannon entropy under \(\nu\), in bits and with values in \([0, \infty]\), of the coordinate \(((x, y), s) \mapsto y\) given the sigma-algebra generated by the coordinate \(((x, y), s) \mapsto s\).

noncomputable def generalConditionalEntropy {X Y S : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace S]
    (ν : ProbabilityMeasure ((X × Y) × S)) : ℝ≥0∞ :=
  conditionalShannonEntropy ν auxiliaryConditioning (fun z => z.1.2) measurable_fst.snd

Uses 2

Statement usesSigma-algebra of the auxiliary coordinate · Conditional Shannon entropy given a sub-\(\sigma\)-algebra

DefinitionConditional entropy of the output given input and auxiliary variable#✓fully proved

For a probability measure \(\nu\) on \((X \times Y) \times S\), \(H(Y \mid X, S)\) is the conditional Shannon entropy under \(\nu\), in bits and with values in \([0, \infty]\), of the coordinate \(((x, y), s) \mapsto y\) given the sigma-algebra generated by the map \(((x, y), s) \mapsto (x, s)\) into \(X \times S\).

noncomputable def generalRecoveryEntropy {X Y S : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace S]
    (ν : ProbabilityMeasure ((X × Y) × S)) : ℝ≥0∞ :=
  conditionalShannonEntropy ν inputAuxiliaryConditioning (fun z => z.1.2) measurable_fst.snd

Uses 2 · Used by 3

Statement usesConditional Shannon entropy given a sub-\(\sigma\)-algebra · Sigma-algebra of the input and auxiliary coordinates

Used byA functional representation has a measurable recovery map · Functional representation of a joint law · A functional representation has the prescribed joint law

DefinitionFunctional representation of a joint law#✓fully proved

Let \(\mu\) be a probability measure on \(X \times Y\) and \(\nu\) a probability measure on \((X \times Y) \times S\). Then \(\nu\) is a functional representation of \(\mu\) when all of the following hold: the image of \(\nu\) under \(((x, y), s) \mapsto (x, y)\) is \(\mu\); the mutual information of the image of \(\nu\) under \(((x, y), s) \mapsto (x, s)\) is zero; the conditional entropy \(H(Y \mid X, S)\) of \(\nu\) is zero; and there is a measurable map \(g : X \times S \to Y\) with \(g(x, s) = y\) for \(\nu\)-almost every \(((x, y), s)\).

def IsGeneralRepresentation {X Y S : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace S]
    (μ : ProbabilityMeasure (X × Y)) (ν : ProbabilityMeasure ((X × Y) × S)) : Prop :=
  ν.map Prod.fst = μ ∧
    measureMutualInformation (ν.map (fun z => (z.1.1, z.2))) = 0 ∧
    generalRecoveryEntropy ν = 0 ∧
    ∃ g : X × S → Y, Measurable g ∧
      ∀ᵐ z ∂ν.toMeasure, g (z.1.1, z.2) = z.1.2

Uses 2 · Used by 2

Statement usesConditional entropy of the output given input and auxiliary variable · Mutual information of a joint probability measure

Used byA functional representation has a measurable recovery map · A functional representation has the prescribed joint law

TheoremA functional representation has the prescribed joint law#✓fully proved

Let \(\mu\) be a probability measure on \(X \times Y\) and let \(\nu\) be a probability measure on \((X \times Y) \times S\) that is a functional representation of \(\mu\). Then the image of \(\nu\) under the projection \(((x, y), s) \mapsto (x, y)\) is \(\mu\).

theorem IsGeneralRepresentation.marginal_eq {X Y S : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace S]
    {μ : ProbabilityMeasure (X × Y)} {ν : ProbabilityMeasure ((X × Y) × S)}
    (h : IsGeneralRepresentation μ ν) : ν.map Prod.fst = μ

Uses 3

Statement usesFunctional representation of a joint law

Proof usesConditional entropy of the output given input and auxiliary variable · Mutual information of a joint probability measure

TheoremA functional representation has a measurable recovery map#✓fully proved

Let \(\mu\) be a probability measure on \(X \times Y\) and let \(\nu\) be a probability measure on \((X \times Y) \times S\) that is a functional representation of \(\mu\). Then there is a measurable map \(g : X \times S \to Y\) such that \(g(x, s) = y\) for \(\nu\)-almost every \(((x, y), s)\).

theorem IsGeneralRepresentation.exists_recovery {X Y S : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace S]
    {μ : ProbabilityMeasure (X × Y)} {ν : ProbabilityMeasure ((X × Y) × S)}
    (h : IsGeneralRepresentation μ ν) :
    ∃ g : X × S → Y, Measurable g ∧ ∀ᵐ z ∂ν.toMeasure, g (z.1.1, z.2) = z.1.2

Uses 3

Statement usesFunctional representation of a joint law

Proof usesConditional entropy of the output given input and auxiliary variable · Mutual information of a joint probability measure

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.