FiniteEntropy.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.entropyTerm line 12
Source documentation
Shannon entropy in bits; the value at mass zero is zero.
Also declared: ComparatorChallenges/SmoothObstruction.lean:12 (same declaration text).
```
noncomputable def entropyTerm (p : ℝ) : ℝ := -(p * Real.log p) / Real.log 2
…
```
def OAI.SmoothObstruction.FiniteEntropy.natEntropy line 18
def OAI.SmoothObstruction.FiniteEntropy.bits line 19
lemma OAI.SmoothObstruction.FiniteEntropy.bits_eq line 21
lemma OAI.SmoothObstruction.FiniteEntropy.negMulLog_le_cross line 27
Source documentation
The pointwise log-sum bound, including the zero convention.
```
lemma negMulLog_le_cross {p q : ℝ} (hp : 0 ≤ p) (hq : 0 < q) :
    Real.negMulLog p ≤ -p * Real.log q + q - p := by
…
```

lemma OAI.SmoothObstruction.FiniteEntropy.sum_negMulLog_le_mass line 41

Source documentation

Entropy of a nonnegative vector of total mass θ on a finite set.

lemma sum_negMulLog_le_mass (s : Finset α) (p : α → ℝ)
    (hp : ∀ i ∈ s, 0 ≤ p i) :
    ∑ i ∈ s, Real.negMulLog (p i) ≤
      Real.negMulLog (∑ i ∈ s, p i) + (∑ i ∈ s, p i) * Real.log s.card := by
…

lemma OAI.SmoothObstruction.FiniteEntropy.entropy_nonneg line 74
lemma OAI.SmoothObstruction.FiniteEntropy.entropy_le_log_card line 83

lemma OAI.SmoothObstruction.FiniteEntropy.entropy_mixture line 88

Source documentation

Concavity of finite entropy, without any independence assumptions.

lemma entropy_mixture [Fintype α] [Fintype β] (w : α → ℝ) (p : α → β → ℝ)
    (hw : ∀ a, 0 ≤ w a) (hsum : ∑ a, w a = 1) (hp : ∀ a b, 0 ≤ p a b) :
    ∑ a, w a * natEntropy (p a) ≤ natEntropy (fun b => ∑ a, w a * p a b) := by
…

Mentions: OAI.SmoothObstruction.FiniteEntropy.natEntropy

lemma OAI.SmoothObstruction.FiniteEntropy.entropy_joint line 100

Source documentation

Exact entropy chain rule for a finite mixture with the component label retained.

lemma entropy_joint [Fintype α] [Fintype β] (w : α → ℝ) (p : α → β → ℝ)
    (hsum : ∀ a, ∑ b, p a b = 1) :
    natEntropy (fun ab : α × β => w ab.1 * p ab.1 ab.2) =
      natEntropy w + ∑ a, w a * natEntropy (p a) := by
…

Mentions: OAI.SmoothObstruction.FiniteEntropy.natEntropy

lemma OAI.SmoothObstruction.FiniteEntropy.negMulLog_le_log_two line 107
def OAI.SmoothObstruction.FiniteEntropy.heavyMass line 117
Source documentation
The high-atom mass of a finite law at threshold exp(-a log L).
```
noncomputable def heavyMass [Fintype α] (a : ℝ) (p : α → ℝ) : ℝ :=
…
```
lemma OAI.SmoothObstruction.FiniteEntropy.heavyMass_nonneg line 120
lemma OAI.SmoothObstruction.FiniteEntropy.heavyMass_le_one line 128
theorem OAI.SmoothObstruction.FiniteEntropy.entropy_le_heavy line 135
Source documentation
The source heavy--light entropy estimate, with its literal one-bit cost.
```
theorem entropy_le_heavy [Fintype α] [Nonempty α] {p : α → ℝ}
    (hp : ∀ i, 0 ≤ p i) (hsum : ∑ i, p i = 1) (a : ℝ) :
    natEntropy p ≤ Real.log 2 +
      (1 - (1 - a) * heavyMass a p) * Real.log (Fintype.card α) := by
…
```
Mentions: OAI.SmoothObstruction.FiniteEntropy.natEntropy, OAI.SmoothObstruction.FiniteEntropy.heavyMass
def OAI.SmoothObstruction.FiniteEntropy.leftMass line 197
def OAI.SmoothObstruction.FiniteEntropy.rightMass line 198
lemma OAI.SmoothObstruction.FiniteEntropy.leftMass_nonneg line 201
lemma OAI.SmoothObstruction.FiniteEntropy.rightMass_nonneg line 204
lemma OAI.SmoothObstruction.FiniteEntropy.le_leftMass line 207
lemma OAI.SmoothObstruction.FiniteEntropy.le_rightMass line 210
lemma OAI.SmoothObstruction.FiniteEntropy.sum_leftMass line 212
lemma OAI.SmoothObstruction.FiniteEntropy.sum_rightMass line 214
theorem OAI.SmoothObstruction.FiniteEntropy.entropy_subadd line 220
Source documentation
Finite joint entropy subadditivity, including zero marginal masses. This is the unconditional entropy input for block-rate existence.
```
theorem entropy_subadd {p : α × β → ℝ} (hp : ∀ x, 0 ≤ p x) (hs : ∑ x, p x = 1) :
    natEntropy p ≤ natEntropy (leftMass p) + natEntropy (rightMass p) := by
…
```
Mentions: OAI.SmoothObstruction.FiniteEntropy.natEntropy, OAI.SmoothObstruction.FiniteEntropy.leftMass, OAI.SmoothObstruction.FiniteEntropy.rightMass
def OAI.SmoothObstruction.FiniteEntropy.pushMass line 254
Source documentation
Pushing a finite entropy vector through a deterministic map cannot increase entropy. There is no measurability or independence assumption.
```
noncomputable def pushMass (p : α → ℝ) (f : α → β) (b : β) : ℝ := by
…
```
lemma OAI.SmoothObstruction.FiniteEntropy.pushMass_nonneg line 259
lemma OAI.SmoothObstruction.FiniteEntropy.sum_pushMass line 269
lemma OAI.SmoothObstruction.FiniteEntropy.entropy_push_le line 275
lemma OAI.SmoothObstruction.FiniteEntropy.entropy_option line 313
Source documentation
Entropy of a symbol emitted only on an event of total mass δ. The marker cost is exactly one natural-log bit; zeros are included.
```
lemma entropy_option {p : Option α → ℝ} (hp : ∀ a, 0 ≤ p a) (hs : ∑ a, p a = 1) :
    natEntropy p ≤ Real.log 2 + (∑ a, p (some a)) * Real.log (Fintype.card α) := by
…
```
Mentions: OAI.SmoothObstruction.FiniteEntropy.natEntropy
lemma OAI.SmoothObstruction.FiniteEntropy.entropy_lower_mass line 341
lemma OAI.SmoothObstruction.FiniteEntropy.entropy_add_le line 346
lemma OAI.SmoothObstruction.FiniteEntropy.entropy_common_le line 359
Source documentation
Removing part of a probability law can increase unnormalized entropy only by the entropy term of the retained mass.
```
lemma entropy_common_le {p m : α → ℝ} (_hp : ∀ a, 0 ≤ p a) (hs : ∑ a, p a=1)
    (hm : ∀ a, 0 ≤ m a) (hmle : ∀ a, m a ≤ p a) :
    natEntropy m ≤ natEntropy p + Real.negMulLog (∑ a,m a) := by
…
```
Mentions: OAI.SmoothObstruction.FiniteEntropy.natEntropy
theorem OAI.SmoothObstruction.FiniteEntropy.entropy_tv line 386
Source documentation
Shannon's continuity estimate from a literal total-variation distance. No coupling or chain-rule inequality is assumed. Natural logs here; division by log 2 gives precisely the manuscript's one-bit cost.
```
theorem entropy_tv {p q : α → ℝ} (hp : ∀ a,0≤p a) (hq : ∀ a,0≤q a)
    (hps : ∑ a,p a=1) (hqs : ∑ a,q a=1) :
    natEntropy q ≤ natEntropy p+Real.log 2+
      ((1/2:ℝ)*∑ a,|p a-q a|)*Real.log (Fintype.card α) := by
…
```
Mentions: OAI.SmoothObstruction.FiniteEntropy.natEntropy