Channel
Difficulty: moderate — 4 definitions, 2 abbreviations, 1 lemmas, 2 theorems.
A channel: a Component.Impl.Simplex (one wire in, one wire out) together with its clock rate (steps per second) — enough extra information to talk about bits per second, not just bits per step.
Channel
A channel: a component with one wire in and one wire out, together with how many steps it takes per second (its clock rate).
structure Channel (State Wire : Type) [Nonempty State] [Norm State] [Nonempty Wire] [Norm Wire] where component : Component.Impl.Simplex State Wire Wire rate : Nat
Outer dependencies: (none)
Inner dependencies: Component.Impl.Simplex, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks
Mathlib dependencies: Norm
Channel.system
A channel’s component, viewed as a plain information system on bare wire values instead of one-element wire bundles — everything below is easier to state this way.
abbrev Channel.system (ch : Channel State Wire) : InformationSystem State Wire Wire := ch.component.toInformationSystem
Outer dependencies: Channel, InformationSystem
Inner dependencies: Component.Impl.Simplex.toInformationSystem
Mathlib dependencies: Norm
Lean core dependencies: Nonempty
maxWireSize
The largest amount of information a single wire can carry: the measure of the biggest value Wire can take. Needs Wire to have finitely many values, so “biggest” is well-defined.
def maxWireSize (Wire : Type) [Fintype Wire] [Nonempty Wire] [Norm Wire] : ℝ := Finset.univ.sup' Finset.univ_nonempty (fun w : Wire => ‖w‖)
Outer dependencies: (none)
Mathlib dependencies: Finset.sup', Finset.univ, Finset.univ_nonempty, Fintype, Norm, Real
Lean core dependencies: Nonempty
Used by: Channel.capacity
Channel.capacity
A channel’s nominal capacity, in bits per second: how much information could get through per second if the wire always carried its largest possible value and nothing were lost along the way. This is an upper bound on what any use of the channel could achieve, not the true Shannon capacity, which properly accounts for noise using probability. See Channel.lossless below for the other half of the picture: what actually gets lost, as opposed to what could in principle get through.
def Channel.capacity [Fintype Wire] (ch : Channel State Wire) : ℝ := ch.rate * maxWireSize Wire
Outer dependencies: Channel
Inner dependencies: maxWireSize
Used by: (none)
Channel.loss
How much information one step reveals to the state instead of the output — the part a receiver watching only the output wire can never see, i.e. genuinely lost from its point of view. Reuses InformationSystem.delta: a positive delta means the step kept more than it revealed.
abbrev Channel.loss (ch : Channel State Wire) (s : State) (w : Wire) : ℝ := ch.system.delta s w
Outer dependencies: Channel
Inner dependencies: Channel.system, InformationSystem.delta
Lean core dependencies: Nonempty
Used by: Channel.lossless, Channel.lossy_loses_overall
Channel.lossless
A channel is lossless exactly when it never hides anything from the receiver: every step reveals everything it took in, so loss is always zero.
def Channel.lossless (ch : Channel State Wire) : Prop := ∀ s w, ch.loss s w = 0
Outer dependencies: Channel
Inner dependencies: Channel.loss
Used by: Channel.lossless_stationary
Channel.overall_loss
Running a channel over a whole run loses exactly the sum of what each individual step lost — this is a direct consequence of InformationSystem.eval_delta, already proved for any information system.
theorem Channel.overall_loss (ch : Channel State Wire) (s : State) (ws : List Wire) : ‖(ch.system.eval s ws).1‖ - ‖s‖ = totalSize ws - totalSize ((ch.system.eval s ws).2) :=
Dependencies: Channel, Channel.system, InformationSystem.eval, totalSize
Proof dependencies: InformationSystem.eval_delta
Used by: (none)
Channel.lossless_stationary
A lossless channel never grows or shrinks its state: since nothing is ever hidden away, the state has nothing new to hold onto.
theorem Channel.lossless_stationary (ch : Channel State Wire) (hl : ch.lossless) (s : State) (w : Wire) : (ch.system.step s w).1 = s := by
Dependencies: Channel, Channel.lossless, Channel.system
Mathlib dependencies: Norm
Used by: (none)
Channel.lossy_loses_overall
A channel that is not lossless drops information somewhere: there’s some run over which what came out carries strictly less information than what went in.
theorem Channel.lossy_loses_overall (ch : Channel State Wire) (s : State) (w : Wire) (hloss : ch.loss s w > 0) : ∃ ws : List Wire, totalSize ws > totalSize ((ch.system.eval s ws).2) := by
Dependencies: Channel, Channel.loss, Channel.system, InformationSystem.eval, totalSize
Used by: (none)
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.