InformationTheory

InformationTheory.Probability.TwoSidedExtension.PastBlockJointLaw

source

Imports 19

Bridge to conditionalEntropyTail #

The remaining piece of the integral identity is matching the μZ-side condExp formulation of condProbPast with the μ-side condDistrib formulation of conditionalEntropyTail. We bridge through:

  • pastBlock k : (∀ _ : ℤ, α) → (Fin k → α), the projection x ↦ (x(-k), x(-k+1), …, x(-1)); viewing the finite past as a finite-dimensional RV;
  • condDistrib_ae_eq_condExp to identify condProbPast a k with (condDistrib coord0 (pastBlock k) (μZ) (pastBlock k x)).real {a};
  • a stationarity-driven joint-law equality between the μZ-pushforward of (coord0, pastBlock k) and the μ-pushforward of (obs k, blockRV k), which transports condEntropy between the two sides via condEntropy_eq_pushforward.
def

InformationTheory.Shannon.TwoSided.pastBlock

source
{α : Type u_2} (k : ℕ) :
(ℤ → α) → Fin k → α

The "past block" projection: pastBlock k x i := x (i.val - k). Maps x : ℤ → α to its restriction at indices {-k, -k+1, …, -1}, viewed as a function Fin k → α.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.TwoSided.measurable_pastBlock

      source
      {α : Type u_2} [MeasurableSpace α] (k : ℕ) :
      Measurable (pastBlock k)

      The past block projection is measurable.

      Used by
        theorem

        InformationTheory.Shannon.TwoSided.comap_pastBlock_eq_pastSigma

        source
        {α : Type u_2} [MeasurableSpace α] (k : ℕ) :
        MeasurableSpace.comap (pastBlock k) MeasurableSpace.pi = pastSigma k

        The comap of MeasurableSpace.pi along pastBlock k equals pastSigma k. This is the algebraic identification of the "past block" σ-algebra with the generator-form pastSigma k.

        Used by

          Joint-law identification via stationarity #

          theorem

          InformationTheory.Shannon.TwoSided.mapZ_coord0_pastBlock_apply_singleton

          source
          {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) (a : α) (s : Fin k → α) :
          (MeasureTheory.Measure.map (fun (x : ℤ → α) => (coord0 x, pastBlock k x)) (μZ μ p)) {(a, s)} = (MeasureTheory.Measure.map (p.blockRV (k + 1)) μ) {Fin.snoc s a}
          Used by
            theorem

            InformationTheory.Shannon.TwoSided.map_obs_blockRV_apply_singleton

            source
            {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) (p : StationaryProcess μ α) (k : ℕ) (a : α) (s : Fin k → α) :
            (MeasureTheory.Measure.map (fun (ω : Ω) => (p.obs k ω, p.blockRV k ω)) μ) {(a, s)} = (MeasureTheory.Measure.map (p.blockRV (k + 1)) μ) {Fin.snoc s a}
            Used by
              theorem

              InformationTheory.Shannon.TwoSided.joint_pastBlock_coord0_eq

              source
              {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (k : ℕ) :
              MeasureTheory.Measure.map (fun (x : ℤ → α) => (coord0 x, pastBlock k x)) (μZ μ p) = MeasureTheory.Measure.map (fun (ω : Ω) => (p.obs k ω, p.blockRV k ω)) μ

              Joint-law equality (the key bridge for the integral identity).

              The pushforward of μZ under the joint map x ↦ (coord0 x, pastBlock k x) equals the pushforward of μ under ω ↦ (p.obs k ω, p.blockRV k ω).

              Proof: both sides are probability measures on α × (Fin k → α). We show they agree on rectangles {a} ×ˢ {s}, which is enough since the spaces are finite. The LHS rectangle reduces, via stationarity (shift by k), to the marginal at the index set {0, 1, …, k}, which equals the ℕ-side block. The RHS rectangle is exactly the singleton mass of μ.map (p.blockRV (k+1)) at the corresponding Fin (k+1) → α.

              Used by
                theorem

                InformationTheory.Shannon.TwoSided.condProbPast_ae_eq_condDistrib

                source
                {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : StationaryProcess μ α) (a : α) (k : ℕ) :
                condProbPast μ p a k =ᵐ[μZ μ p] fun (x : ℤ → α) => ((ProbabilityTheory.condDistrib coord0 (pastBlock k) (μZ μ p)) (pastBlock k x)).real {a}

                Conditional expectation identification: condProbPast a k agrees a.s. with the condDistrib-form regular conditional probability built from (coord0, pastBlock k).

                Used by