`cert`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.LDPCCodeRateFromPhi
domain: Information
line: 101 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.LDPCCodeRateFromPhi on GitHub at line 101.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  98    gapToCapacity (2 * N) = gapToCapacity N / 2
  99  gap_N_invariant : ∀ {N : ℝ}, 0 < N → gapToCapacity N * N = 1 / phi
 100
 101def cert : LDPCRateCert where
 102  gap_pos := gap_pos
 103  gap_monotone := gap_decreasing
 104  doubling_halves := gap_doubling_halves
 105  gap_N_invariant := gap_times_N_invariant
 106
 107end
 108
 109end LDPCCodeRateFromPhi
 110end Information
 111end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.