Conditional-fiber entropy estimates

A finite log-sum inequality proves Korten's entropy lemma (Lemma 4). A bijection with the full-cube fiber verifies the dimension convention. Markov's inequality gives the 63/64 good-fiber estimate needed in the improved mirror-set argument.

theorem Complexity.BooleanAnalysis.mul_log_tangent_internal {a c : ℝ} (ha : 0 ≤ a) (hc : 0 < c) : a * Real.log c + a - c ≤ a * Real.log a

theorem Complexity.BooleanAnalysis.sum_mul_log_ge_internal {β : Type u_1} [Fintype β] [Nonempty β] {m : β → ℝ} (hm : ∀ (b : β), 0 ≤ m b) (hpos : 0 < ∑ b : β, m b) : (∑ b : β, m b) * Real.log ((∑ b : β, m b) / ↑(Fintype.card β)) ≤ ∑ b : β, m b * Real.log (m b)

theorem Complexity.BooleanAnalysis.expect_log_card_fiber_internal {α : Type u_1} {β : Type u_2} [Fintype β] [Nonempty β] (X : Finset α) (hX : X.Nonempty) (g : α → β) : Real.log ↑X.card - Real.log ↑(Fintype.card β) ≤ X.expect fun (x : α) => Real.log ↑{y ∈ X | g y = g x}.card

theorem Complexity.BooleanAnalysis.card_coordinateFiber_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : (coordinateFiber X s x).card = {y ∈ X | (fun (i : { i : ι // s i ≠ true }) => y ↑i) = fun (i : { i : ι // s i ≠ true }) => x ↑i}.card

theorem Complexity.BooleanAnalysis.coordinateFiber_nonempty_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Finset (ι → Bool)} (s : ι → Bool) {x : ι → Bool} (hx : x ∈ X) : (coordinateFiber X s x).Nonempty

theorem Complexity.BooleanAnalysis.uniformDeficit_nonneg_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) : 0 ≤ uniformDeficit X

theorem Complexity.BooleanAnalysis.expect_uniformDeficit_coordinateFiber_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (hX : X.Nonempty) (s : ι → Bool) : (X.expect fun (x : ι → Bool) => uniformDeficit (coordinateFiber X s x)) ≤ uniformDeficit X

theorem Complexity.BooleanAnalysis.coordinateFiber_good_probability_internal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (hX : X.Nonempty) (s : ι → Bool) {k : ℝ} (hk : 0 < k) (hdef : uniformDeficit X ≤ k) : 63 / 64 ≤ X.expect fun (x : ι → Bool) => if uniformDeficit (coordinateFiber X s x) ≤ 64 * k then 1 else 0

theorem Complexity.BooleanAnalysis.sum_uniformMass_internal {α : Type u_1} [Fintype α] [DecidableEq α] {X : Finset α} (hX : X.Nonempty) : ∑ x : α, uniformMass X x = 1

theorem Complexity.BooleanAnalysis.sum_uniformMass_mul_internal {α : Type u_1} [Fintype α] [DecidableEq α] (X : Finset α) (f : α → ℝ) : ∑ x : α, uniformMass X x * f x = X.expect fun (x : α) => f x

theorem Complexity.BooleanAnalysis.card_eq_rpow_sub_uniformDeficit_internal {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) : ↑X.card = 2 ^ (↑(Fintype.card ι) - uniformDeficit X)

theorem Complexity.BooleanAnalysis.uniformDeficit_le_iff_internal {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) {k : ℝ} : uniformDeficit X ≤ k ↔ 2 ^ (↑(Fintype.card ι) - k) ≤ ↑X.card

theorem Complexity.BooleanAnalysis.uniformMass_le_rpow_internal {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) {k : ℝ} (hdef : uniformDeficit X ≤ k) (x : ι → Bool) : uniformMass X x ≤ 2 ^ (k - ↑(Fintype.card ι))