High edge cost forces a strict entropy decrease

Lax263307.EntropyDecrease · concepts/Lax263307/EntropyDecrease.lean · lax-263307

proven

Loading review…

Let $y\in R_r(G,k)$ , $k>0$ , $|A|<r$ , and $y_A>0$ . For a positive integer $p$ , if the conditioned costs satisfy

\sum_{uv\in E(G)}x_u x_v>k^2/p,

then some vertex $v$ has $\pi_v>0$ and conditioning on $v$ decreases entropy by more than $2/p$ :

H(\pi^v)<H(\pi)-2/p.

Concept map

6 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

Show types on hover

1	import Lax263307.ConditioningDistribution
2	import Lax263307.EntropyGap
3
4	/-!
5	---
6	title: High edge cost forces a strict entropy decrease
7	type: theorem
8	---
9	Let $y\in R_r(G,k)$ , $k>0$ , $\|A\|<r$ , and $y_A>0$ .
10	For a positive integer $p$ , if the conditioned costs satisfy
11	$\sum_{uv\in E(G)}x_u x_v>k^2/p,$
12	then some vertex $v$ has $\pi_v>0$ and conditioning on $v$ decreases entropy
13	by more than $2/p$ :
14	$H(\pi^v)<H(\pi)-2/p.$
15
16	# Attribution
17
18	Bonnet–Chang, proof of Lemma 12, the consequence of equation (18).
19	-/
20
21	namespace Lax263307.EntropyDecrease
22
23	open LinearRelaxation ConditioningDistribution Entropy
24
25	/-- An expensive edge product forces a positive-cost conditioning step. -/
26	axiom exists_entropy_decrease {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
27	(k r p : ℕ) (y : MomentVector n r) (feasible : IsFeasible G k r y)
28	(A : Finset (Fin n)) (size : A.card < r) (positive : 0 < value y A)
29	(target_positive : 0 < k) (threshold_positive : 0 < p)
30	(expensive : (k : ℝ) ^ 2 / p < edgeCost G (conditioned y A)) :
31	∃ v : Fin n, 0 < marginal y A k v ∧
32	entropy (marginal y (insert v A) k) < entropy (marginal y A k) - 2 / p
33
34	end Lax263307.EntropyDecrease
35

Bonnet–Chang, proof of Lemma 12, the consequence of equation (18).

Builds on

Used by

From Mathlib

none

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive