InformationTheory.Shannon.ParallelGaussian.PerCoordRegularity
Parallel Gaussian capacity: regularity bundle and hypothesis-minimal headline #
Assembles the regularity bundle IsParallelGaussianPerCoordRegularity (3 fields:
bddAbove / achiever_mi / max_ent) from named lemmas, and re-publishes the capacity
formula in hypothesis-minimal form.
Main statements #
isParallelGaussianPerCoordRegularity_of_pieces— assembles the regularity bundle from its three constituent fields.parallel_gaussian_capacity_formula_minimal— the capacity formula with the regularity bundle assembled internally, so its only inputs are the KKT conditionh_kktand the power-positivity / measurability preconditions.
Regularity bundle constructor #
InformationTheory.Shannon.ParallelGaussian.isParallelGaussianPerCoordRegularity_of_pieces
source{n : ℕ}
(P : ℝ)
(hP : 0 ≤ P)
(N : Fin n → NNReal)
(hN : ∀ (i : Fin n), ↑(N i) ≠ 0)
(h_meas : IsParallelAwgnChannelMeasurable N)
(h_parallel_meas : IsParallelGaussianKernelMeasurable N)
(Q : Fin n → NNReal)
:
IsParallelGaussianPerCoordRegularity P N h_meas h_parallel_meas Q
Assemble the regularity bundle IsParallelGaussianPerCoordRegularity from its three
constituent fields.
Used by
Hypothesis-minimal headline #
InformationTheory.Shannon.ParallelGaussian.parallel_gaussian_capacity_formula_minimal
source{n : ℕ}
(P : ℝ)
(hP : 0 < P)
(N : Fin (n + 1) → NNReal)
(hN : ∀ (i : Fin (n + 1)), ↑(N i) ≠ 0)
(h_meas : IsParallelAwgnChannelMeasurable N)
(h_parallel_meas : IsParallelGaussianKernelMeasurable N)
(ν : ℝ)
(h_kkt : IsWaterFillingKKT P N ν)
:
parallelGaussianCapacity P N h_meas h_parallel_meas = ∑ i : Fin (n + 1), 1 / 2 * Real.log (1 + waterFillingPower ν N i / ↑(N i))
Parallel Gaussian channel capacity (water-filling), hypothesis-minimal form. The
parallel Gaussian capacity equals the water-filling sum at the KKT water level ν. The
regularity bundle is assembled internally, so the only inputs are the KKT condition h_kkt
and the preconditions hP / hN / h_meas / h_parallel_meas.