OAI/Probability/SphericalField/Control/SmoothTerminals.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.FiniteTerminal line 25
2. def OAI.SphericalPerceptron.finiteTerminalVariational line 28
3. lemma OAI.SphericalPerceptron.finiteTerminal_one line 32
4. lemma OAI.SphericalPerceptron.finiteTerminalVariational_bounds line 38
5. lemma OAI.SphericalPerceptron.finiteTerminalVariational_coe_toReal line 55
6. lemma OAI.SphericalPerceptron.terminalVariational_eq_finiteTerminal line 62
7. def OAI.SphericalPerceptron.Jet3.ofCompactSmooth line 102
8. lemma OAI.SphericalPerceptron.Jet3.ofCompactSmooth_apply line 115
9. lemma OAI.SphericalPerceptron.exists_bounded_smooth_terminal line 118
10. lemma OAI.SphericalPerceptron.exists_bounded_smooth_terminal_sequence line 148
11. lemma OAI.SphericalPerceptron.finiteTerminalVariational_toReal_sub_le line 173
12. lemma OAI.SphericalPerceptron.finiteTerminalVariational_abs_sub_le line 197
13. lemma OAI.SphericalPerceptron.terminalVariational_eq_finiteTerminal_continuous line 207