Lean 4 Formalization of JSD Contraction Coefficients: Core Definitions and Theorems

Key Points

• The aim is to formalize definitions and theorems related to Jensen-Shannon divergence contraction coefficients in Lean 4.
• Utilized Lean 4 for formal verification of mathematical definitions.
• Incorporated Mathlib for supporting mathematical libraries.
• Defined key parameters: s_m, λ_m, η_JSD, and η_χ².
• Established and verified theorems for binary equality and the BSC formula.
• Confirmed exact formulas for contraction coefficients using formal methods.
• Validated the binary equality case for m=2.
• Reinforced m-ary symmetric channel formula with formal proofs.