OAI/Computability/VertexCover/Information/Pinsker.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Information.hellingerSquared line 45
2. theorem OAI.UniqueGames.Foundations.Information.sqrt_distance_le_relativeEntropy_term line 48
3. theorem OAI.UniqueGames.Foundations.Information.hellingerSquared_le_relativeEntropy line 73
4. theorem OAI.UniqueGames.Foundations.Information.totalVariation_sq_le_hellingerSquared line 81
5. theorem OAI.UniqueGames.Foundations.Information.totalVariation_sq_le_relativeEntropy line 106
6. theorem OAI.UniqueGames.Foundations.Information.posterior_totalVariation_sq_le_log line 112