OAI/Probability/IsingPerceptron/VarianceDerivative.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Variance Derivative.

  1. lemma OAI.IsingPerceptron.hasDerivWithinAt_sqrt_comp_zero line 16
  2. lemma OAI.IsingPerceptron.hasDerivWithinAt_sqrt_comp line 47
  3. theorem OAI.IsingPerceptron.hasDerivWithinAt_random_cylinder_variance line 60
  4. lemma OAI.IsingPerceptron.gaussian_sum_identDistrib line 95
  5. lemma OAI.IsingPerceptron.random_cgf_insertion_eq line 125
  6. lemma OAI.IsingPerceptron.scalarShiftLaw_amplitude line 158
  7. def OAI.IsingPerceptron.edgeGaussianTag line 171
  8. lemma OAI.IsingPerceptron.edgeGaussianTag_injective line 174
  9. def OAI.IsingPerceptron.edgeGaussianCoordinates line 178
  10. lemma OAI.IsingPerceptron.edgeGaussianCoordinates_preserving line 181
  11. def OAI.IsingPerceptron.scalarCoordinateInsert line 188
  12. lemma OAI.IsingPerceptron.scalarCoordinateInsert_preserving line 194
  13. lemma OAI.IsingPerceptron.forestVertexDepth_edgeAt line 226
  14. def OAI.IsingPerceptron.labelLevelCoefficients line 232
  15. lemma OAI.IsingPerceptron.cascadeCoordinateEnergy_insert line 236
  16. lemma OAI.IsingPerceptron.labelLevelCoefficients_diag line 254
  17. lemma OAI.IsingPerceptron.labelLevelCoefficients_bound line 259
  18. lemma OAI.IsingPerceptron.labelLevelCoefficients_cross line 264
  19. lemma OAI.IsingPerceptron.externalFieldCoefficients_cross line 285
  20. lemma OAI.IsingPerceptron.monotone_field_add line 291
  21. lemma OAI.IsingPerceptron.field_add_nonneg line 296
  22. lemma OAI.IsingPerceptron.enrichedCoefficients_field_add_cross line 299
  23. lemma OAI.IsingPerceptron.enriched_field_add_law line 313
  24. lemma OAI.IsingPerceptron.referenceReplicaMean_fold line 337
  25. def OAI.IsingPerceptron.enrichedHamiltonian line 354
  26. lemma OAI.IsingPerceptron.measurable_enrichedHamiltonian line 360
  27. def OAI.IsingPerceptron.enrichedReplicaAverage line 373
  28. lemma OAI.IsingPerceptron.measurable_enrichedReplicaMean line 380
  29. lemma OAI.IsingPerceptron.enrichedHamiltonian_insert line 392
  30. theorem OAI.IsingPerceptron.enrichedReplicaAverage_eq_random line 405
  31. def OAI.IsingPerceptron.enrichedFieldFunctional line 447
  32. lemma OAI.IsingPerceptron.measurable_enrichedFieldFunctional line 453
  33. def OAI.IsingPerceptron.enrichedGibbsReference line 470
  34. instance OAI.IsingPerceptron.enrichedGibbsReference_probability line 475
  35. lemma OAI.IsingPerceptron.measurable_enrichedGibbsReference line 481
  36. def OAI.IsingPerceptron.enrichedFieldInsertedPressure line 489
  37. lemma OAI.IsingPerceptron.enrichedFieldInsertedPressure_law line 496
  38. lemma OAI.IsingPerceptron.enrichedField_cgf_eq line 511
  39. lemma OAI.IsingPerceptron.enrichedMeanPressure_field_insert line 548
  40. lemma OAI.IsingPerceptron.randomReplicaAverage_zero_fold line 581
  41. theorem OAI.IsingPerceptron.enrichedMeanPressure_field_derivative line 601