OAI/Probability/SphericalField/Control/HeatChain.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.SphericalPerceptron.HeatChain line 16
2. lemma OAI.SphericalPerceptron.HeatChain.left_le_right line 22
3. lemma OAI.SphericalPerceptron.controls_equal_prefix line 28
4. lemma OAI.SphericalPerceptron.controls_equal_cost_prefix line 38
5. lemma OAI.SphericalPerceptron.HeatChain.upper line 47
6. lemma OAI.SphericalPerceptron.HeatChain.lower line 63
7. lemma OAI.SphericalPerceptron.controlledPrefix_one line 95
8. lemma OAI.SphericalPerceptron.controlledPrefix_zero line 101
9. lemma OAI.SphericalPerceptron.intervalControlCost_full line 108