Shannon.Entropy.Approx

Phase 3 of the characterization: continuity extension.

Constructs floor-count rational approximants approxProb p N and proves their convergence to p. This is the bridge from the rational formula to the full real-probability formula.

Phase 3: Continuity Extension by Rational Approximation

noncomputable def LeanPool.Shannon1948Formalization.approxCount {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) (a : α) : ℕ

Integer count approximation used in the continuity-extension phase.

Equations

• LeanPool.Shannon1948Formalization.approxCount p N a = ⌊↑(N + 1) * ↑p a⌋₊ + 1

noncomputable def LeanPool.Shannon1948Formalization.approxTotal {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) : ℕ

Total count for approxCount; this is the denominator of the rational approximation.

Equations

• LeanPool.Shannon1948Formalization.approxTotal p N = ∑ a : α, LeanPool.Shannon1948Formalization.approxCount p N a

theorem LeanPool.Shannon1948Formalization.approxCount_pos {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) (a : α) : 0 < approxCount p N a

theorem LeanPool.Shannon1948Formalization.approxTotal_pos {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) : 0 < approxTotal p N

noncomputable def LeanPool.Shannon1948Formalization.approxProb {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) : ProbDist α

Rational approximation of p obtained from floor counts.

Equations

• LeanPool.Shannon1948Formalization.approxProb p N = ⟨fun (a : α) => ↑(LeanPool.Shannon1948Formalization.approxCount p N a) / ↑(LeanPool.Shannon1948Formalization.approxTotal p N), ⋯⟩

@[simp]

theorem LeanPool.Shannon1948Formalization.approxProb_apply {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) (a : α) : ↑(approxProb p N) a = ↑(approxCount p N a) / ↑(approxTotal p N)

theorem LeanPool.Shannon1948Formalization.entropyNat_approxProb (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) : H (approxProb p N) = (-K fun {α : Type} [Fintype α] => H) * ∑ a : α, ↑(approxProb p N) a * Real.log (↑(approxProb p N) a)

theorem LeanPool.Shannon1948Formalization.approxCount_mul_bounds {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) (a : α) : have M := ↑(N + 1); 0 ≤ ↑(approxCount p N a) - M * ↑p a ∧ ↑(approxCount p N a) - M * ↑p a ≤ 1

theorem LeanPool.Shannon1948Formalization.approxTotal_bounds {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) : have M := ↑(N + 1); 0 ≤ ↑(approxTotal p N) - M ∧ ↑(approxTotal p N) - M ≤ ↑(Fintype.card α)

theorem LeanPool.Shannon1948Formalization.approxProb_error_bound {α : Type} [Fintype α] (p : ProbDist α) (N : ℕ) (a : α) : have M := ↑(N + 1); |↑(approxProb p N) a - ↑p a| ≤ (↑(Fintype.card α) + 1) / M

theorem LeanPool.Shannon1948Formalization.tendsto_approxProb_apply {α : Type} [Fintype α] (p : ProbDist α) (a : α) : Filter.Tendsto (fun (N : ℕ) => ↑(approxProb p N) a) Filter.atTop (nhds (↑p a))

theorem LeanPool.Shannon1948Formalization.tendsto_approxProb {α : Type} [Fintype α] (p : ProbDist α) : Filter.Tendsto (fun (N : ℕ) => approxProb p N) Filter.atTop (nhds p)