OAI/Probability/Perceptron/Variational/FieldDerivative.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SphericalPerceptronFreeEnergy.sourceFeature_square_boundline 12 - lemma
OAI.SphericalPerceptronFreeEnergy.sourceKernelPressure_gaussianMean_baseline 17 - theorem
OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_right_derivativeline 43 - def
OAI.SphericalPerceptronFreeEnergy.sourceFieldObservableline 76 - lemma
OAI.SphericalPerceptronFreeEnergy.sourceFieldObservable_measurableline 80 - lemma
OAI.SphericalPerceptronFreeEnergy.sourceFieldObservable_boundline 90 - lemma
OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_observable_boundline 97 - lemma
OAI.SphericalPerceptronFreeEnergy.sourceConditional_field_observable_integrableline 107 - lemma
OAI.SphericalPerceptronFreeEnergy.sourceConditional_partition_pos_aeline 121 - lemma
OAI.SphericalPerceptronFreeEnergy.tiltMean_const_of_posline 135 - lemma
OAI.SphericalPerceptronFreeEnergy.sourceConditional_response_eqline 143