OAI/Probability/IsingPerceptron/FiniteGaussianVariation.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Finite Gaussian Variation.

  1. structure OAI.IsingPerceptron.AffineGaussianStep line 15
  2. def OAI.IsingPerceptron.gaussianFamilyFold line 24
  3. def OAI.IsingPerceptron.boundarySlope line 29
  4. def OAI.IsingPerceptron.boundaryCoefficient line 33
  5. def OAI.IsingPerceptron.variationWeights line 37
  6. def OAI.IsingPerceptron.gaussianFoldCertificate line 42
  7. lemma OAI.IsingPerceptron.boundarySlope_eq_neg_sum line 49
  8. lemma OAI.IsingPerceptron.gaussianFamilyFold_value line 55
  9. lemma OAI.IsingPerceptron.GaussianFamily.time_derivative line 65
  10. lemma OAI.IsingPerceptron.VariationCertificate.time_nonpos line 71
  11. theorem OAI.IsingPerceptron.gaussianFold_decreases line 82
  12. def OAI.IsingPerceptron.affineVarianceFloor line 114
  13. def OAI.IsingPerceptron.affineVarianceDomain line 116
  14. lemma OAI.IsingPerceptron.affineVarianceDomain_open line 119
  15. lemma OAI.IsingPerceptron.affineVarianceFloor_pos line 124
  16. lemma OAI.IsingPerceptron.affineVarianceDomain_segment line 128
  17. def OAI.IsingPerceptron.finiteAffineStep line 139
  18. def OAI.IsingPerceptron.variationWeightAt line 162
  19. lemma OAI.IsingPerceptron.variationWeightAt_zero line 165
  20. lemma OAI.IsingPerceptron.variationWeightAt_succ line 169
  21. def OAI.IsingPerceptron.ofFnWeights line 177
  22. def OAI.IsingPerceptron.afterCoefficient line 180
  23. lemma OAI.IsingPerceptron.boundarySlope_ofFn line 183
  24. lemma OAI.IsingPerceptron.ofFnWeights_zero line 188
  25. lemma OAI.IsingPerceptron.ofFnWeights_succ line 198
  26. lemma OAI.IsingPerceptron.afterCoefficient_succ line 203
  27. lemma OAI.IsingPerceptron.ofFnWeights_eq line 209
  28. lemma OAI.IsingPerceptron.FinTailNonneg_ofFnWeights line 221
  29. lemma OAI.IsingPerceptron.finite_delta_sum line 243
  30. lemma OAI.IsingPerceptron.finite_tail_delta_sum line 252
  31. lemma OAI.IsingPerceptron.continuous_gaussianTransform_param line 279
  32. lemma OAI.IsingPerceptron.continuous_gaussianFold_param line 326
  33. structure OAI.IsingPerceptron.BoundedC2Data line 360
  34. def OAI.IsingPerceptron.BoundedC2Data.family line 375
  35. lemma OAI.IsingPerceptron.BoundedC2Data.continuous line 378
  36. def OAI.IsingPerceptron.nodalGaussianFold line 381
  37. def OAI.IsingPerceptron.nextCoefficient line 385
  38. theorem OAI.IsingPerceptron.nodalGaussianFold_antitone_strict line 390
  39. lemma OAI.IsingPerceptron.continuous_nodalGaussianFold_param line 446
  40. theorem OAI.IsingPerceptron.nodalGaussianFold_antitone line 477
  41. def OAI.IsingPerceptron.uniformNodal line 534
  42. def OAI.IsingPerceptron.uniformCoefficient line 537
  43. lemma OAI.IsingPerceptron.uniformNodal_zero line 539
  44. lemma OAI.IsingPerceptron.uniformNodal_last line 542
  45. lemma OAI.IsingPerceptron.uniformNodal_value line 545
  46. lemma OAI.IsingPerceptron.uniformNodal_increasing line 549
  47. lemma OAI.IsingPerceptron.uniformCoefficient_nonneg line 565
  48. lemma OAI.IsingPerceptron.uniformCoefficient_difference line 569
  49. lemma OAI.IsingPerceptron.uniformWeight_castSucc line 576
  50. lemma OAI.IsingPerceptron.uniformWeight_last line 583
  51. lemma OAI.IsingPerceptron.uniformPattern_eq_nodal line 588