OAI/Probability/SphericalField/Fields/CoupledDual.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.Trial.ext_fun line 13
2. lemma OAI.SphericalPerceptron.weightedStepTrial_coupling_fst line 19
3. lemma OAI.SphericalPerceptron.weightedStepTrial_coupling_snd line 33
4. lemma OAI.SphericalPerceptron.coupling_sum_fst line 47
5. lemma OAI.SphericalPerceptron.coupling_sum_snd line 53
6. lemma OAI.SphericalPerceptron.weightedStepTail_coupling_fst line 59
7. lemma OAI.SphericalPerceptron.weightedStepA_coupling_fst line 65
8. lemma OAI.SphericalPerceptron.entropy_coupled_stationary_comparison line 71
9. lemma OAI.SphericalPerceptron.finiteSphericalDual_eq_stationary line 115
10. theorem OAI.SphericalPerceptron.finiteSphericalDual_abs_sub_le line 125