OAI/Probability/IsingPerceptron/ContactFaces.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Contact Faces.

  1. lemma OAI.IsingPerceptron.enrichedContactObjective_faces line 16
  2. lemma OAI.IsingPerceptron.contact_small_cost line 51
  3. theorem OAI.IsingPerceptron.enriched_contact_eventually_lower line 60
  4. lemma OAI.IsingPerceptron.finiteFieldPath_zero line 106
  5. theorem OAI.IsingPerceptron.enriched_step_upper_tolerance line 112
  6. lemma OAI.IsingPerceptron.pathAmplitude_zero line 159
  7. lemma OAI.IsingPerceptron.enrichedCoefficients_zero line 162
  8. lemma OAI.IsingPerceptron.enrichedCylinderPressure_zero line 172
  9. def OAI.IsingPerceptron.finiteRowPressure line 181
  10. lemma OAI.IsingPerceptron.enrichedFixed_mean_zero line 185
  11. lemma OAI.IsingPerceptron.enrichedMeanPressure_zero line 196
  12. lemma OAI.IsingPerceptron.spinLaw_singleton line 207
  13. lemma OAI.IsingPerceptron.spinLaw_integral line 214
  14. lemma OAI.IsingPerceptron.abs_nat_sequence_sub line 229
  15. lemma OAI.IsingPerceptron.poisson_sequence_integrable line 246
  16. lemma OAI.IsingPerceptron.poisson_coupling_bound line 259
  17. lemma OAI.IsingPerceptron.finiteRowPressure_mean_step line 287
  18. lemma OAI.IsingPerceptron.poisson_error_tendsto line 304
  19. def OAI.IsingPerceptron.expectedPressure line 330
  20. lemma OAI.IsingPerceptron.gaussian_matrix_preserving line 333
  21. lemma OAI.IsingPerceptron.finiteRowPressure_gaussian line 348
  22. lemma OAI.IsingPerceptron.measurable_pressure line 360
  23. lemma OAI.IsingPerceptron.finiteRowPressure_mean_gaussian line 375
  24. theorem OAI.IsingPerceptron.gaussian_step_upper_tolerance line 394
  25. def OAI.IsingPerceptron.uniformCut line 428
  26. lemma OAI.IsingPerceptron.uniformCut_strict line 430
  27. lemma OAI.IsingPerceptron.uniformCut_zero line 435
  28. lemma OAI.IsingPerceptron.uniformCut_last line 436
  29. def OAI.IsingPerceptron.lowerGrid line 440
  30. lemma OAI.IsingPerceptron.lowerGrid_factor_nonneg line 443
  31. lemma OAI.IsingPerceptron.lowerGrid_monotone line 448
  32. lemma OAI.IsingPerceptron.lowerGrid_mem line 455
  33. lemma OAI.IsingPerceptron.lowerGrid_le line 464
  34. lemma OAI.IsingPerceptron.uniformCell_ae line 473
  35. lemma OAI.IsingPerceptron.floor_on_uniformCell line 496
  36. lemma OAI.IsingPerceptron.lowerGrid_step_ae line 507
  37. lemma OAI.IsingPerceptron.lowerGrid_ae_tendsto line 515
  38. lemma OAI.IsingPerceptron.lowerGrid_integral_tendsto line 524
  39. lemma OAI.IsingPerceptron.stepFunction_nonneg line 546
  40. lemma OAI.IsingPerceptron.stepFunction_bound line 553
  41. lemma OAI.IsingPerceptron.measurable_stepFunction line 562
  42. lemma OAI.IsingPerceptron.overlapPath_bound line 565
  43. lemma OAI.IsingPerceptron.stepFunction_mul_path_integrable line 571
  44. theorem OAI.IsingPerceptron.isingEntropy_mono line 582
  45. lemma OAI.IsingPerceptron.gaussianFamilyFold_KX line 603
  46. lemma OAI.IsingPerceptron.VariationCertificate.time_bound line 609
  47. lemma OAI.IsingPerceptron.gaussianFold_lipschitz line 625