OAI/Probability/Perceptron/Variational/DepthLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptronFreeEnergy.indexedInfiniteLeafMeasure line 11
  2. instance OAI.SphericalPerceptronFreeEnergy.indexedInfiniteLeafMeasure_probability line 16
  3. def OAI.SphericalPerceptronFreeEnergy.indexedDepthArray line 21
  4. lemma OAI.SphericalPerceptronFreeEnergy.indexedDepthArray_measurable line 24
  5. def OAI.SphericalPerceptronFreeEnergy.indexedDepthLaw line 36
  6. lemma OAI.SphericalPerceptronFreeEnergy.indexedDepthLaw_lintegral line 40
  7. lemma OAI.SphericalPerceptronFreeEnergy.indexedDepthLaw_lintegral_prefix line 53
  8. lemma OAI.SphericalPerceptronFreeEnergy.infiniteReplica_prefix_fresh_preserving line 68
  9. lemma OAI.SphericalPerceptronFreeEnergy.indexedDepthLaw_geometry line 83
  10. def OAI.SphericalPerceptronFreeEnergy.CascadeShapeReplicas line 92
  11. instance OAI.SphericalPerceptronFreeEnergy.cascadeShapeReplicas_fintype line 96
  12. def OAI.SphericalPerceptronFreeEnergy.cascadeShapeLeaves line 104
  13. lemma OAI.SphericalPerceptronFreeEnergy.cascadeShapeReplicas_nonempty line 109
  14. lemma OAI.SphericalPerceptronFreeEnergy.cascadeShapeReplicas_card line 118
  15. def OAI.SphericalPerceptronFreeEnergy.cascadeShapeReplicasOfFnEquiv line 130
  16. lemma OAI.SphericalPerceptronFreeEnergy.cascadeShapeLeaves_cast line 138
  17. lemma OAI.SphericalPerceptronFreeEnergy.cascadeShapeLeaves_ofFn line 145
  18. theorem OAI.SphericalPerceptronFreeEnergy.finite_leaf_tuple_shape line 156