Conditioning with a quantitative moment lower bound
Lax263307.HeavyConditioning · concepts/Lax263307/HeavyConditioning.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
A high edge cost forces entropy decrease even after conditioning choices with extremely small marginal probability are excluded. Some choice of probability at least tau=1/(2np(log2 n+1)) decreases entropy by more than 1/p. Within r≥p(log2 n+1) steps, a sparse conditioning set is therefore reached with raw moment at least tau^r.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax263307.ConditioningExistence |
| 2 | import Mathlib.Data.Nat.Log |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Conditioning with a quantitative moment lower bound |
| 7 | type: theorem |
| 8 | --- |
| 9 | A high edge cost forces entropy decrease even after conditioning choices |
| 10 | with extremely small marginal probability are excluded. Some choice of |
| 11 | probability at least tau=1/(2np(log2 n+1)) decreases entropy by more than |
| 12 | 1/p. Within r≥p(log2 n+1) steps, a sparse conditioning set is therefore |
| 13 | reached with raw moment at least tau^r. |
| 14 | |
| 15 | # Formalization notes |
| 16 | |
| 17 | This strengthens the positive-moment existence guarantee. The quantitative |
| 18 | lower bound prevents a violated component inequality from having an |
| 19 | arbitrarily small raw gap at a feasible query. It is used by the strong-gap |
| 20 | ellipsoid argument; exact rational enumeration remains a separate step. |
| 21 | -/ |
| 22 | |
| 23 | namespace Lax263307.HeavyConditioning |
| 24 | |
| 25 | open LinearRelaxation ConditioningDistribution Entropy |
| 26 | |
| 27 | noncomputable def probabilityFloor (n p : ℕ) : ℝ := |
| 28 | 1 / (2 * (n : ℝ) * p * ((Nat.log2 n : ℝ) + 1)) |
| 29 | |
| 30 | axiom heavy_entropy_decrease {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 31 | (k r p : ℕ) (y : MomentVector n r) (feasible : IsFeasible G k r y) |
| 32 | (A : Finset (Fin n)) (size : A.card < r) (positive : 0 < value y A) |
| 33 | (target_positive : 0 < k) (threshold_positive : 0 < p) (order_positive : 0 < n) |
| 34 | (expensive : (k : ℝ) ^ 2 / p < edgeCost G (conditioned y A)) : |
| 35 | ∃ v : Fin n, probabilityFloor n p ≤ marginal y A k v ∧ |
| 36 | entropy (marginal y (insert v A) k) < entropy (marginal y A k) - 1 / p |
| 37 | |
| 38 | axiom heavy_low_edge_cost {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 39 | (k r p : ℕ) (y : MomentVector n r) (feasible : IsFeasible G k r y) |
| 40 | (order_positive : 0 < n) (target_positive : 0 < k) |
| 41 | (level_positive : 0 < r) (threshold_positive : 0 < p) |
| 42 | (budget : (p : ℝ) * ((Nat.log2 n : ℝ) + 1) ≤ r) : |
| 43 | ∃ A : Finset (Fin n), A.card ≤ r ∧ probabilityFloor n p ^ r ≤ value y A ∧ |
| 44 | 0 < value y A ∧ (∀ v, 0 ≤ conditioned y A v ∧ conditioned y A v ≤ 1) ∧ |
| 45 | (∑ v, conditioned y A v) = k ∧ edgeCost G (conditioned y A) ≤ (k : ℝ) ^ 2 / p |
| 46 | |
| 47 | end Lax263307.HeavyConditioning |
| 48 |
Formalization notes
This strengthens the positive-moment existence guarantee. The quantitative lower bound prevents a violated component inequality from having an arbitrarily small raw gap at a feasible query. It is used by the strong-gap ellipsoid argument; exact rational enumeration remains a separate step.
Builds on
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments