InformationTheory

InformationTheory.Shannon.Pi

source

Imports 2

Shared Pi-type plumbing for Shannon information theory #

MeasurableEquiv invariance of entropy/condEntropy under re-indexing of Pi-type random variables, together with condEntropy ≥ 0 and subset-split measurable equivalences.

Main definitions #

  • subsetSplitMEquivAux — ((↥T₁ → α) × (↥R → α)) ≃ᵐ (↥U → α) for disjoint T₁, R with T₁ ∪ R = U.

Main statements #

Implementation notes #

MeasurableEquiv.coe_piFinsetUnion, piFinsetUnion_apply_left/right lift Equiv.piFinsetUnion_left/_right into the MeasurableEquiv namespace for use in Pi-type reshape proofs across the Shannon moonshot files.

theorem

InformationTheory.Shannon.entropy_measurableEquiv_comp

source
{Ω : Type u_2} [MeasurableSpace Ω] {β : Type u_3} {γ : Type u_4} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (μ : MeasureTheory.Measure Ω) (Xs : Ω → β) (hXs : Measurable Xs) (e : β ≃ᵐ γ) :
(entropy μ fun (ω : Ω) => e (Xs ω)) = entropy μ Xs
Used by
    theorem

    InformationTheory.Shannon.condEntropy_measurableEquiv_comp

    source
    {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] {β : Type u_3} {γ : Type u_4} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xc : Ω → α) (hXc : Measurable Xc) (Yo : Ω → β) (hYo : Measurable Yo) (e : β ≃ᵐ γ) :
    (MeasureFano.condEntropy μ Xc fun (ω : Ω) => e (Yo ω)) = MeasureFano.condEntropy μ Xc Yo
    Used by

      Basic inequality for conditional entropy #

      theorem

      InformationTheory.Shannon.condEntropy_nonneg

      source
      {Ω : Type u_2} [MeasurableSpace Ω] {W : Type u_3} [Fintype W] [Nonempty W] [MeasurableSpace W] [MeasurableSingletonClass W] {Y : Type u_4} [MeasurableSpace Y] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Ws : Ω → W) (Yo : Ω → Y) :
      0 ≤ MeasureFano.condEntropy μ Ws Yo
      Used by

        Subset reshape index equivalences #

        theorem

        MeasurableEquiv.coe_piFinsetUnion

        source
        @[simp]
        {ι : Type u_3} [DecidableEq ι] {β : ι → Type u_4} [(i : ι) → MeasurableSpace (β i)] {s t : Finset ι} (h : Disjoint s t) :
        ⇑(piFinsetUnion β h) = ⇑(Equiv.piFinsetUnion β h)
        Used by
          theorem

          MeasurableEquiv.piFinsetUnion_apply_left

          source
          {ι : Type u_3} [DecidableEq ι] {β : ι → Type u_4} [(i : ι) → MeasurableSpace (β i)] {s t : Finset ι} (h : Disjoint s t) {f : (i : ↥s) → β ↑i} {g : (i : ↥t) → β ↑i} {i : ι} (hi : i ∈ s) (hi' : i ∈ s ∪ t) :
          (piFinsetUnion β h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩
          Used by
            theorem

            MeasurableEquiv.piFinsetUnion_apply_right

            source
            {ι : Type u_3} [DecidableEq ι] {β : ι → Type u_4} [(i : ι) → MeasurableSpace (β i)] {s t : Finset ι} (h : Disjoint s t) {f : (i : ↥s) → β ↑i} {g : (i : ↥t) → β ↑i} {i : ι} (hi : i ∈ t) (hi' : i ∈ s ∪ t) :
            (piFinsetUnion β h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩
            Used by
              def

              InformationTheory.Shannon.subsetSplitMEquivAux

              source
              {ι : Type u_3} [DecidableEq ι] {β : ι → Type u_4} [(i : ι) → MeasurableSpace (β i)] {T₁ R U : Finset ι} (hd : Disjoint T₁ R) (hU : T₁ ∪ R = U) :
              ((i : ↥T₁) → β ↑i) × ((i : ↥R) → β ↑i) ≃ᵐ ((i : ↥U) → β ↑i)

              The measurable equivalence ((↥T₁ → α) × (↥R → α)) ≃ᵐ (↥U → α) for disjoint T₁, R with T₁ ∪ R = U. Composed from MeasurableEquiv.piFinsetUnion and MeasurableEquiv.cast.

              Equations
              Instances For
                Used by
                  theorem

                  InformationTheory.Shannon.subsetSplitMEquivAux_apply

                  source
                  {α : Type u_1} [MeasurableSpace α] {n : ℕ} {T₁ R U : Finset (Fin n)} (hd : Disjoint T₁ R) (hU : T₁ ∪ R = U) (Xs : Fin n → α) :
                  (subsetSplitMEquivAux hd hU) (fun (j : ↥T₁) => Xs ↑j, fun (j : ↥R) => Xs ↑j) = fun (j : ↥U) => Xs ↑j
                  Used by