OAI/Probability/SKRatio/Gaussian/HammingGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Calculus.hammingDist_real_sum line 14
2. lemma OAI.SKRatio.Calculus.hamming_exp_sum line 19
3. def OAI.SKRatio.Calculus.spinVector line 34
4. lemma OAI.SKRatio.Calculus.spinVector_norm_sq line 37
5. lemma OAI.SKRatio.Calculus.spinVector_sub_norm_sq line 40
6. lemma OAI.SKRatio.Calculus.hamiltonian_eq_inner line 48
7. lemma OAI.SKRatio.Calculus.abs_hamiltonian_sub_hamming line 55
8. lemma OAI.SKRatio.Calculus.mass_le_of_hamming line 86
9. lemma OAI.SKRatio.Calculus.hamming_ball_exp_bound line 110
10. def OAI.SKRatio.Calculus.hammingNeighborhood line 129
11. lemma OAI.SKRatio.Calculus.gibbs_hamming_neighborhood line 132
12. lemma OAI.SKRatio.Calculus.exists_small_hamming_radius line 177
13. def OAI.SKRatio.Calculus.hammingTo line 199
14. lemma OAI.SKRatio.Calculus.hammingTo_attained line 202
15. lemma OAI.SKRatio.Calculus.hammingTo_le line 207
16. lemma OAI.SKRatio.Calculus.hammingTo_zero_of_mem line 213
17. lemma OAI.SKRatio.Calculus.hammingTo_triangle line 218
18. lemma OAI.SKRatio.Calculus.hammingTo_le_radius_iff line 224
19. lemma OAI.SKRatio.Calculus.hammingDist_replace_le_one line 236
20. def OAI.SKRatio.Calculus.distanceObservable line 247
21. lemma OAI.SKRatio.Calculus.distanceObservable_nonneg line 250
22. lemma OAI.SKRatio.Calculus.distanceObservable_zero line 253
23. lemma OAI.SKRatio.Calculus.unweightedGradient_distanceObservable line 256
24. lemma OAI.SKRatio.Calculus.distanceObservable_mean_lower line 294