OAI/NumberTheory/PrimePackets/ConditionalShannon.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.finiteShannon_mul line 17
2. lemma OAI.PrimeDegreePackets.finiteShannon_mass_decomposition line 24
3. theorem OAI.PrimeDegreePackets.finiteShannon_joint_mass_le line 47

   Source documentation

   Subadditivity for a nonnegative finite measure; its total mass need not be one.

   theorem finiteShannon_joint_mass_le {α β : Type*} [Fintype α] [Fintype β]
       (p : α × β → ℝ) (hp : ∀ z, 0 ≤ p z) :
       finiteShannon p + Real.negMulLog (∑ z, p z) ≤
         finiteShannon (fun a => ∑ b, p (a,b)) +
         finiteShannon (fun b => ∑ a, p (a,b)) := by
   …

   Mentions: OAI.PrimeDegreePackets.finiteShannon

4. theorem OAI.PrimeDegreePackets.finiteShannon_submodular line 80

   Source documentation

   The finite entropy submodularity inequality H(ABC)+H(A) ≤ H(AB)+H(AC).

   theorem finiteShannon_submodular {α β γ : Type*}
       [Fintype α] [Fintype β] [Fintype γ]
       (p : α × (β × γ) → ℝ) (hp : ∀ z, 0 ≤ p z) :
       finiteShannon p + finiteShannon (fun a => ∑ z : β × γ, p (a,z)) ≤
         finiteShannon (fun z : α × β => ∑ c, p (z.1,(z.2,c))) +
         finiteShannon (fun z : α × γ => ∑ b, p (z.1,(b,z.2))) := by
   …

   Mentions: OAI.PrimeDegreePackets.finiteShannon

5. lemma OAI.PrimeDegreePackets.finiteShannon_fst_le line 90
6. lemma OAI.PrimeDegreePackets.finiteShannon_joint_decomposition line 97