InformationTheory

InformationTheory.Shannon.LpPointwise

source

Imports 6

Lifting an L² class to a genuine pointwise representative #

The matched-filter receiver of a continuous-time AWGN code (ContAwgnCode) needs its test functions to be honest ℝ → ℝ functions: testFn_support asks for the support to lie in [0, T] everywhere (not just a.e.), and testFn_orthonormal states orthonormality as a pointwise Lebesgue integral ∫ t, gᵢ t · gⱼ t, not an L² inner product. The spectral assets that produce the family, however, live in Lp as a.e.-equivalence classes.

This file bridges that gap for the real space Lp ℝ 2 volume. Given an f : Lp ℝ 2 volume whose a.e. representative already vanishes a.e. off a measurable set s, its s-indicator ptRepr s f := s.indicator (⇑f) is a genuine function that

The a.e. agreement turns the pointwise product integral into the L² inner product (integral_ptRepr_mul), which upgrades an orthonormal family in Lp ℝ 2 volume (supported a.e. in [0, T]) to a pointwise-orthonormal family of [0, T]-supported functions (exists_pointwise_orthonormal_of_orthonormal) — exactly the three ContAwgnCode.testFn regularity fields.

noncomputable def

InformationTheory.Shannon.LpPointwise.ptRepr

source
(s : Set ℝ) (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) :
ℝ → ℝ

The pointwise representative of an L² class f, cut down to the set s: the genuine function s.indicator (⇑f). When ⇑f already vanishes a.e. off s, this loses no L² content (ptRepr_ae_eq) but gains an everywhere support bound (support_ptRepr_subset).

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.LpPointwise.support_ptRepr_subset

      source
      (s : Set ℝ) (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) :
      Function.support (ptRepr s f) ⊆ s

      ptRepr s f is supported in s everywhere (it is an s-indicator).

      Used by
        theorem

        InformationTheory.Shannon.LpPointwise.memLp_ptRepr

        source
        {s : Set ℝ} (hs : MeasurableSet s) (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) :
        MeasureTheory.MemLp (ptRepr s f) 2 MeasureTheory.volume

        ptRepr s f still lies in L².

        Used by
          theorem

          InformationTheory.Shannon.LpPointwise.ptRepr_ae_eq

          source
          {s : Set ℝ} (hs : MeasurableSet s) (f : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (hf : ↑↑f =ᵐ[MeasureTheory.volume.restrict sᶜ] 0) :
          ptRepr s f =ᵐ[MeasureTheory.volume] ↑↑f

          If ⇑f vanishes a.e. off s, then ptRepr s f agrees with ⇑f a.e.

          Used by
            theorem

            InformationTheory.Shannon.LpPointwise.integral_ptRepr_mul

            source
            {s : Set ℝ} (hs : MeasurableSet s) (f g : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (hf : ↑↑f =ᵐ[MeasureTheory.volume.restrict sᶜ] 0) (hg : ↑↑g =ᵐ[MeasureTheory.volume.restrict sᶜ] 0) :
            ∫ (t : ℝ), ptRepr s f t * ptRepr s g t = inner ℝ f g

            The pointwise product integral of two representatives equals the L² inner product of the underlying classes, provided both vanish a.e. off s.

            Used by
              theorem

              InformationTheory.Shannon.LpPointwise.exists_pointwise_orthonormal_of_orthonormal

              source
              {k : ℕ} {T : ℝ} (e : Fin k → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (he : Orthonormal ℝ e) (hsupp : ∀ (i : Fin k), ↑↑(e i) =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 T)ᶜ] 0) :
              ∃ (g : Fin k → ℝ → ℝ), (∀ (i : Fin k), Function.support (g i) ⊆ Set.Icc 0 T) ∧ (∀ (i : Fin k), MeasureTheory.MemLp (g i) 2 MeasureTheory.volume) ∧ ∀ (i j : Fin k), ∫ (t : ℝ), g i t * g j t = if i = j then 1 else 0

              An orthonormal family in Lp ℝ 2 volume, each member supported a.e. in [0, T], lifts to a family of genuine ℝ → ℝ functions that satisfy the three ContAwgnCode.testFn regularity fields: everywhere-support in [0, T], MemLp, and pointwise orthonormality ∫ t, gᵢ t · gⱼ t = δᵢⱼ.

              Used by