ChannelCapacity.StrictConcavity #
Strict concavity infrastructure on the simplex of probability measures.
Mathlib does not currently equip ProbabilityMeasure α with an affine or vector-space structure, so
strict concavity is phrased directly in terms of the explicit operation
ProbabilityMeasure.convexCombination.
theorem
ProbabilityMeasure.eq_of_isMaxOn_univ_of_strictConcave
{α : Type u_1}
[MeasurableSpace α]
{f : MeasureTheory.ProbabilityMeasure α → ℝ}
(hStrict :
∀ (p q : MeasureTheory.ProbabilityMeasure α),
p ≠ q → ∀ (t : NNReal), 0 < t → ∀ (ht_lt_one : t < 1), f (convexCombination p q t ⋯) > ↑t * f p + (1 - ↑t) * f q)
{p q : MeasureTheory.ProbabilityMeasure α}
(hp : IsMaxOn f Set.univ p)
(hq : IsMaxOn f Set.univ q)
:
Two global maximizers coincide if the function is strictly concave along convex combinations of probability measures.
theorem
ProbabilityMeasure.convexCombination_comm
{α : Type u_1}
[MeasurableSpace α]
(p q : MeasureTheory.ProbabilityMeasure α)
(t : NNReal)
(ht : t ≤ 1)
:
theorem
ProbabilityMeasure.eq_left_of_convexCombination_eq
{α : Type u_1}
[MeasurableSpace α]
{p q : MeasureTheory.ProbabilityMeasure α}
{t : NNReal}
(ht_lt_one : t < 1)
(h : convexCombination p q t ⋯ = p)
:
theorem
ProbabilityMeasure.eq_right_of_convexCombination_eq
{α : Type u_1}
[MeasurableSpace α]
{p q : MeasureTheory.ProbabilityMeasure α}
{t : NNReal}
(ht_pos : 0 < t)
(ht_lt_one : t < 1)
(h : convexCombination p q t ⋯ = q)
:
theorem
ProbabilityMeasure.convexCombination_ne_left
{α : Type u_1}
[MeasurableSpace α]
{p q : MeasureTheory.ProbabilityMeasure α}
(h_ne : p ≠ q)
{t : NNReal}
(ht_lt_one : t < 1)
:
theorem
ProbabilityMeasure.convexCombination_ne_right
{α : Type u_1}
[MeasurableSpace α]
{p q : MeasureTheory.ProbabilityMeasure α}
(h_ne : p ≠ q)
{t : NNReal}
(ht_pos : 0 < t)
(ht_lt_one : t < 1)
:
theorem
ChannelCapacity.Kernel.mutualInformation_strictlyConcave_of_injectivePriorPushforward
{α : Type u_3}
{β : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(k : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel k]
(h : InjectivePriorPushforward k)
(hWC : WellConditionedForCapacity k)
(p q : MeasureTheory.ProbabilityMeasure α)
(_h_ne : p ≠ q)
(t : NNReal)
(_ht_pos : 0 < t)
(ht_lt_one : t < 1)
:
mutualInformation (ProbabilityMeasure.convexCombination p q t ⋯) k > ↑t * mutualInformation p k + (1 - ↑t) * mutualInformation q k