Entropy.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.RowColumn.weighted_log_le line 12

Source documentation

The elementary Gibbs inequality in the exact finite form used for the occupied-board product bound. No probability or overlap estimate is assumed.

lemma weighted_log_le {ι : Type*} (s : Finset ι) (p z : ι → ℝ)
    (hp : ∀ i ∈ s, 0 ≤ p i) (hz : ∀ i ∈ s, 0 < z i) :
    ∑ i ∈ s, p i * Real.log (z i) ≤ ∑ i ∈ s, p i * (z i - 1) := by
…

lemma OAI.RowColumn.entropy_le_log_card line 20
Source documentation
Entropy of a distribution on k symbols is at most log k, including zero probabilities. This is the marginal-entropy step in both grid proofs.
```
lemma entropy_le_log_card {ι : Type*} [Fintype ι] (p : ι → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hs : ∑ i, p i = 1) :
    -∑ i, p i * Real.log (p i) ≤ Real.log (Fintype.card ι) := by
…
```
def OAI.RowColumn.uniformMarginal line 53
Source documentation
Marginal of the uniform distribution on ι along an actual line map.
```
def uniformMarginal {ι α : Type*} [Fintype ι] [DecidableEq α] (f : ι → α) (a : α) : ℝ :=
…
```
lemma OAI.RowColumn.uniformMarginal_nonneg line 56
lemma OAI.RowColumn.sum_uniformMarginal_mul line 62
lemma OAI.RowColumn.sum_uniformMarginal line 70
lemma OAI.RowColumn.uniformMarginal_pos line 74
lemma OAI.RowColumn.sum_over_embedding_le line 83

theorem OAI.RowColumn.occupied_product_of_mean_le line 94

Source documentation

The exact exp(number of holes) product loss. The marginals are computed from the actual occupied embedding, so arbitrary deletion patterns are covered. This is the entropy/quarter-root normalization step of weighted.tex:143–150 and coherent.tex:191–205.

theorem occupied_product_of_mean_le {ι α β : Type*}
    [Fintype ι] [Fintype α] [Fintype β]
    [DecidableEq α] [DecidableEq β]
    (e : ι ↪ α × β) (z : α → β → ℝ) (hz : ∀ a b, 0 ≤ z a b)
    (hmean : ∑ a, ∑ b,
      uniformMarginal (fun i => (e i).1) a * uniformMarginal (fun i => (e i).2) b * z a b ≤ 1) :
    ∏ i, z (e i).1 (e i).2 ≤
      Real.exp ((Fintype.card α * Fintype.card β - Fintype.card ι : ℕ) : ℝ) := by
…

Mentions: OAI.RowColumn.uniformMarginal