OAI/Probability/SphericalPerceptron/PressureComparison.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

Spherical pressure comparisons for invariant operator disorder

The pressure convergence theorem assumes convergence in probability. The Gaussian cavity/contact and global penalty limits, angular limit identification, finite radial Laplace formula, spectral mesh convergence, and unconditional pressure convergence under the spectral hypotheses remain unproved. The variational functionals and limit predicates below define quantities and statements, not proofs of these limits.

  1. abbrev OAI.SphericalPerceptron.InvariantDisorder.Vec line 22
  2. abbrev OAI.SphericalPerceptron.InvariantDisorder.Disorder line 23
  3. def OAI.SphericalPerceptron.InvariantDisorder.spherePoint line 25
  4. lemma OAI.SphericalPerceptron.InvariantDisorder.measurable_spherePoint line 28
  5. def OAI.SphericalPerceptron.InvariantDisorder.sphereMeasure line 32
  6. instance OAI.SphericalPerceptron.InvariantDisorder.(instance at line 35) line 35
  7. def OAI.SphericalPerceptron.InvariantDisorder.rowEnergy line 39
  8. def OAI.SphericalPerceptron.InvariantDisorder.pressure line 42
  9. lemma OAI.SphericalPerceptron.InvariantDisorder.continuous_rowEnergy line 45
  10. lemma OAI.SphericalPerceptron.InvariantDisorder.rowEnergy_abs_le line 50
  11. lemma OAI.SphericalPerceptron.InvariantDisorder.integrable_exp_of_abs_le line 61
  12. lemma OAI.SphericalPerceptron.InvariantDisorder.exp_integral_bounds line 68
  13. lemma OAI.SphericalPerceptron.InvariantDisorder.log_integral_exp_abs_le line 86
  14. lemma OAI.SphericalPerceptron.InvariantDisorder.log_integral_exp_le_add line 96
  15. lemma OAI.SphericalPerceptron.InvariantDisorder.log_integral_exp_sub_abs_le line 116
  16. lemma OAI.SphericalPerceptron.InvariantDisorder.pressure_abs_le line 133
  17. lemma OAI.SphericalPerceptron.InvariantDisorder.continuous_pressure line 144
  18. lemma OAI.SphericalPerceptron.InvariantDisorder.spherePoint_norm_le line 165
  19. lemma OAI.SphericalPerceptron.InvariantDisorder.sphereMeasure_norm_le line 171
  20. lemma OAI.SphericalPerceptron.InvariantDisorder.sphereMeasure_map line 177
  21. lemma OAI.SphericalPerceptron.InvariantDisorder.stdGaussian_vec_zero line 186
  22. lemma OAI.SphericalPerceptron.InvariantDisorder.sphereMeasure_norm_sq line 197
  23. lemma OAI.SphericalPerceptron.InvariantDisorder.sum_abs_le_sqrt_mul_norm line 212
  24. lemma OAI.SphericalPerceptron.InvariantDisorder.rowEnergy_sub_abs_le line 217
  25. theorem OAI.SphericalPerceptron.InvariantDisorder.pressure_operator_stability line 238
  26. lemma OAI.SphericalPerceptron.InvariantDisorder.mean_convergence_of_bounded_in_probability line 262
  27. lemma OAI.SphericalPerceptron.InvariantDisorder.pressure_comp_isometry line 286
  28. lemma OAI.SphericalPerceptron.InvariantDisorder.rowEnergy_activation_error line 299
  29. theorem OAI.SphericalPerceptron.InvariantDisorder.pressure_activation_error line 313
  30. lemma OAI.SphericalPerceptron.InvariantDisorder.activation_error_of_compact_error line 349
  31. theorem OAI.SphericalPerceptron.InvariantDisorder.pressure_compact_activation_error line 370
  32. abbrev OAI.SphericalPerceptron.InvariantDisorder.Sym line 378
  33. abbrev OAI.SphericalPerceptron.InvariantDisorder.Fields line 379
  34. structure OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial line 381
  35. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.increment line 386
  36. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.K line 390
  37. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.Active line 394
  38. instance OAI.SphericalPerceptron.InvariantDisorder.(instance at line 398) line 398
  39. instance OAI.SphericalPerceptron.InvariantDisorder.(instance at line 404) line 404
  40. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.compression line 407
  41. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.baseline line 412
  42. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.Eligible line 417
  43. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.entropy line 427
  44. def OAI.SphericalPerceptron.InvariantDisorder.matrixGaussianStep line 435
  45. def OAI.SphericalPerceptron.InvariantDisorder.MatrixTrial.value line 441
  46. def OAI.SphericalPerceptron.InvariantDisorder.gaussianValues line 447
  47. def OAI.SphericalPerceptron.InvariantDisorder.gaussianFunctional line 452
  48. def OAI.SphericalPerceptron.InvariantDisorder.GaussianWellDefined line 455
  49. def OAI.SphericalPerceptron.InvariantDisorder.angularDim line 459
  50. abbrev OAI.SphericalPerceptron.InvariantDisorder.Coefficients line 460
  51. def OAI.SphericalPerceptron.InvariantDisorder.Coefficients.Admissible line 462
  52. def OAI.SphericalPerceptron.InvariantDisorder.coefficientField line 468
  53. def OAI.SphericalPerceptron.InvariantDisorder.yField line 472
  54. def OAI.SphericalPerceptron.InvariantDisorder.uField line 475
  55. def OAI.SphericalPerceptron.InvariantDisorder.rowTests line 483
  56. def OAI.SphericalPerceptron.InvariantDisorder.testConstants line 489
  57. def OAI.SphericalPerceptron.InvariantDisorder.penaltyTerminal line 494
  58. def OAI.SphericalPerceptron.InvariantDisorder.penaltyBox line 498
  59. def OAI.SphericalPerceptron.InvariantDisorder.penaltyValue line 501
  60. def OAI.SphericalPerceptron.InvariantDisorder.coefficientEntropy line 505
  61. def OAI.SphericalPerceptron.InvariantDisorder.coefficientValues line 511
  62. def OAI.SphericalPerceptron.InvariantDisorder.coefficientFunctional line 516
  63. def OAI.SphericalPerceptron.InvariantDisorder.CoefficientWellDefined line 519
  64. def OAI.SphericalPerceptron.InvariantDisorder.shellEntropy line 528
  65. def OAI.SphericalPerceptron.InvariantDisorder.haarJacobian line 531
  66. abbrev OAI.SphericalPerceptron.InvariantDisorder.AngularFamily line 534
  67. def OAI.SphericalPerceptron.InvariantDisorder.PositiveProportions line 536
  68. def OAI.SphericalPerceptron.InvariantDisorder.AngularFormula line 539
  69. structure OAI.SphericalPerceptron.InvariantDisorder.FiniteSpectrum line 558
  70. def OAI.SphericalPerceptron.InvariantDisorder.InputBlocks line 567
  71. instance OAI.SphericalPerceptron.InvariantDisorder.(instance at line 570) line 570
  72. instance OAI.SphericalPerceptron.InvariantDisorder.(instance at line 575) line 575
  73. def OAI.SphericalPerceptron.InvariantDisorder.finiteBlock line 577
  74. def OAI.SphericalPerceptron.InvariantDisorder.inputWeights line 580
  75. def OAI.SphericalPerceptron.InvariantDisorder.openSimplex line 585
  76. def OAI.SphericalPerceptron.InvariantDisorder.radialObjective line 588
  77. def OAI.SphericalPerceptron.InvariantDisorder.radialValue line 593
  78. def OAI.SphericalPerceptron.InvariantDisorder.RadialWellDefined line 596
  79. def OAI.SphericalPerceptron.InvariantDisorder.outputDimension line 600
  80. def OAI.SphericalPerceptron.InvariantDisorder.slotCount line 601
  81. def OAI.SphericalPerceptron.InvariantDisorder.singularSlots line 603
  82. def OAI.SphericalPerceptron.InvariantDisorder.BiOrthogonallyInvariant line 606
  83. def OAI.SphericalPerceptron.InvariantDisorder.empiricalAverage line 612
  84. def OAI.SphericalPerceptron.InvariantDisorder.outlierError line 615
  85. def OAI.SphericalPerceptron.InvariantDisorder.SpectralHypotheses line 619
  86. def OAI.SphericalPerceptron.InvariantDisorder.PressureConverges line 625
  87. structure OAI.SphericalPerceptron.InvariantDisorder.SpectralMesh line 630
  88. def OAI.SphericalPerceptron.InvariantDisorder.meshMultiplicity line 639
  89. def OAI.SphericalPerceptron.InvariantDisorder.slotDiagonal line 643
  90. def OAI.SphericalPerceptron.InvariantDisorder.HasMeshApproximation line 648
  91. def OAI.SphericalPerceptron.InvariantDisorder.MeshApproximates line 657
  92. def OAI.SphericalPerceptron.InvariantDisorder.HasFiniteSlots line 665
  93. def OAI.SphericalPerceptron.InvariantDisorder.FiniteRadialLimit line 669
  94. def OAI.SphericalPerceptron.InvariantDisorder.SpectralMeshLimit line 681
  95. lemma OAI.SphericalPerceptron.InvariantDisorder.pressure_uniform_bound line 687
  96. theorem OAI.SphericalPerceptron.InvariantDisorder.pressure_converges_of_in_probability line 700