OAI/Probability/IsingPerceptron/VariationalFiniteness.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Variational Finiteness.

  1. lemma OAI.IsingPerceptron.gaussianTransform_zero_variance line 16
  2. lemma OAI.IsingPerceptron.magneticRecursion_zero line 23
  3. lemma OAI.IsingPerceptron.magneticFieldValue_zero line 31
  4. lemma OAI.IsingPerceptron.enrichedMeanPressure_field_add_le line 36
  5. lemma OAI.IsingPerceptron.magneticFieldValue_nonpos line 61
  6. lemma OAI.IsingPerceptron.fieldRecursion_nonpos line 77
  7. def OAI.IsingPerceptron.zeroFieldStep line 103
  8. lemma OAI.IsingPerceptron.fieldRecursion_zeroFieldStep line 107
  9. lemma OAI.IsingPerceptron.stepFunction_zeroFieldStep line 110
  10. lemma OAI.IsingPerceptron.isingEntropy_nonneg line 116
  11. def OAI.IsingPerceptron.zeroOverlapPath line 124
  12. lemma OAI.IsingPerceptron.zeroOverlapPath_ae line 127
  13. lemma OAI.IsingPerceptron.isingEntropy_zero line 130
  14. lemma OAI.IsingPerceptron.gaussianFold_measurable_bounded line 143
  15. lemma OAI.IsingPerceptron.uniformPattern_abs_bound line 155
  16. lemma OAI.IsingPerceptron.patternFunctional_abs_bound line 166
  17. theorem OAI.IsingPerceptron.variationalValue_finite_of_continuous line 174
  18. theorem OAI.IsingPerceptron.variationalValue_real_of_continuous line 196

    Distinct definitions of this name: ComparatorChallenges/IsingFiniteness.lean:86 (same statement text; different proof or body). Qualify references as OAI.IsingPerceptron.variationalValue_real_of_continuous@path.