OAI/Probability/IsingPerceptron/NextRowJoin.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Next Row Join.

  1. def OAI.IsingPerceptron.prefixExtend line 16
  2. lemma OAI.IsingPerceptron.measurable_prefixExtend line 19
  3. lemma OAI.IsingPerceptron.prefixExtend_coe line 26
  4. lemma OAI.IsingPerceptron.integral_next_row_of_prefixInvariant line 29
  5. lemma OAI.IsingPerceptron.measurable_random_cgf_one line 45
  6. def OAI.IsingPerceptron.enrichedFreshRowCGF line 51
  7. lemma OAI.IsingPerceptron.measurable_enrichedFreshRowCGF line 56
  8. lemma OAI.IsingPerceptron.enrichedGibbs_prefix_congr line 66
  9. theorem OAI.IsingPerceptron.enrichedNextPatternCGF_eq_independent line 79
  10. lemma OAI.IsingPerceptron.abs_enrichedFreshRowCGF_le line 120
  11. lemma OAI.IsingPerceptron.enrichedFreshRowCGF_integrable line 126
  12. lemma OAI.IsingPerceptron.enrichedNextPatternCGF_mean line 134
  13. theorem OAI.IsingPerceptron.enrichedMeanPressure_fresh_time_derivative line 158
  14. def OAI.IsingPerceptron.spinRowCoefficients line 182
  15. lemma OAI.IsingPerceptron.spinRowCoefficients_cross line 185
  16. lemma OAI.IsingPerceptron.cylinderField_spinRow line 191
  17. def OAI.IsingPerceptron.gaussianRowActivation line 200
  18. lemma OAI.IsingPerceptron.measurable_gaussianRowActivation line 203
  19. lemma OAI.IsingPerceptron.freshRowCGF_gaussian line 209
  20. theorem OAI.IsingPerceptron.enriched_gaussian_fresh_limit line 219
  21. lemma OAI.IsingPerceptron.left_derivative_nonpos_of_min line 265
  22. theorem OAI.IsingPerceptron.enriched_time_minimum_fresh line 276
  23. theorem OAI.IsingPerceptron.no_interior_contact_sequence line 330
  24. lemma OAI.IsingPerceptron.perturbation_square_sum_le line 411
  25. lemma OAI.IsingPerceptron.enrichedMeanPressure_zero_perturbation_cost line 418
  26. lemma OAI.IsingPerceptron.isingEntropy_chain_lower line 456
  27. lemma OAI.IsingPerceptron.magneticFieldValue_entropy_le line 483
  28. lemma OAI.IsingPerceptron.enrichedMeanPressure_magnetic_upper line 503
  29. lemma OAI.IsingPerceptron.enrichedContactObjective_initial_lower line 517
  30. lemma OAI.IsingPerceptron.enrichedContactObjective_cap_lower line 537
  31. lemma OAI.IsingPerceptron.exists_coercive_sqrt_cap line 598
  32. lemma OAI.IsingPerceptron.contact_cap_exists line 615