OAI/Probability/Perceptron/Variational/FieldDerivative.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptronFreeEnergy.sourceFeature_square_bound line 12
  2. lemma OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure_gaussianMean_base line 17
  3. theorem OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_right_derivative line 43
  4. def OAI.SphericalPerceptronFreeEnergy.sourceFieldObservable line 76
  5. lemma OAI.SphericalPerceptronFreeEnergy.sourceFieldObservable_measurable line 80
  6. lemma OAI.SphericalPerceptronFreeEnergy.sourceFieldObservable_bound line 90
  7. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_observable_bound line 97
  8. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_observable_integrable line 107
  9. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_partition_pos_ae line 121
  10. lemma OAI.SphericalPerceptronFreeEnergy.tiltMean_const_of_pos line 135
  11. lemma OAI.SphericalPerceptronFreeEnergy.sourceConditional_response_eq line 143