OAI/Probability/SphericalField/Control/FiniteValue.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.expected_intervalControlCost_full line 16
  2. lemma OAI.SphericalPerceptron.Jet3.lipschitz line 22
  3. lemma OAI.SphericalPerceptron.HeatChain.controlValue_eq line 28
  4. lemma OAI.SphericalPerceptron.ultrametric_extension_row line 62
  5. lemma OAI.SphericalPerceptron.finite_measure_eq_of_maximal_coordinates line 74
  6. lemma OAI.SphericalPerceptron.finite_ultrametric_row_law_unique line 124
  7. abbrev OAI.SphericalPerceptron.FiniteOverlap line 141
  8. abbrev OAI.SphericalPerceptron.FiniteBlock line 142
  9. def OAI.SphericalPerceptron.finiteBlock line 144
  10. def OAI.SphericalPerceptron.finiteRow line 147
  11. def OAI.SphericalPerceptron.FiniteGG line 150
  12. lemma OAI.SphericalPerceptron.finiteBlock_measurable line 156
  13. lemma OAI.SphericalPerceptron.finiteRow_measurable line 161
  14. def OAI.SphericalPerceptron.finiteFiberRow line 166
  15. lemma OAI.SphericalPerceptron.finiteFiberRow_real line 170