OAI/Probability/SphericalField/Control/Payoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SphericalPerceptron.controlPayoff_compact_bound line 17
2. lemma OAI.SphericalPerceptron.controlValue_le_of_cost_cutoff line 68
3. lemma OAI.SphericalPerceptron.controlValue_compact_bound line 83
4. lemma OAI.SphericalPerceptron.controlValue_uniform_of_compact line 123
5. def OAI.SphericalPerceptron.terminalVariational line 151
6. lemma OAI.SphericalPerceptron.variationalValue_eq_terminal line 154
7. lemma OAI.SphericalPerceptron.terminalVariational_bounds line 157
8. lemma OAI.SphericalPerceptron.terminalVariational_coe_toReal line 175
9. lemma OAI.SphericalPerceptron.terminalVariational_toReal_sub_le line 182
10. lemma OAI.SphericalPerceptron.terminalVariational_abs_sub_le line 205