OAI/Probability/IsingPerceptron/TimeIncrement.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Time Increment.

  1. lemma OAI.IsingPerceptron.enrichedHamiltonian_count_succ line 16
  2. lemma OAI.IsingPerceptron.enrichedFixed_pressure_increment line 27
  3. lemma OAI.IsingPerceptron.enrichedFixed_mean_step_bound line 54
  4. lemma OAI.IsingPerceptron.enrichedMeanPressure_eq_poissonMean line 70
  5. def OAI.IsingPerceptron.enrichedNextPatternCGF line 98
  6. lemma OAI.IsingPerceptron.enrichedFixed_mean_increment line 104
  7. theorem OAI.IsingPerceptron.enrichedMeanPressure_time_derivative line 120
  8. lemma OAI.IsingPerceptron.random_cylinder_cgf_amplitude_cost line 167
  9. lemma OAI.IsingPerceptron.enriched_coordinate_lipschitz line 200
  10. lemma OAI.IsingPerceptron.cube_coordinate_sum_bound line 230
  11. theorem OAI.IsingPerceptron.enrichedMeanPressure_perturbation_lipschitz line 255
  12. lemma OAI.IsingPerceptron.poissonMean_lipschitz line 278
  13. theorem OAI.IsingPerceptron.enrichedMeanPressure_time_lipschitz line 289
  14. abbrev OAI.IsingPerceptron.ContactParameter line 314
  15. def OAI.IsingPerceptron.contactRegion line 316
  16. lemma OAI.IsingPerceptron.contactRegion_nonneg line 320
  17. lemma OAI.IsingPerceptron.contactRegion_mem line 326
  18. lemma OAI.IsingPerceptron.isCompact_contactRegion line 333
  19. lemma OAI.IsingPerceptron.contactRegion_nonempty line 337
  20. lemma OAI.IsingPerceptron.enrichedMeanPressure_parameters_continuousOn line 343
  21. def OAI.IsingPerceptron.enrichedContactObjective line 384
  22. lemma OAI.IsingPerceptron.continuous_enrichedContactPenalty line 391
  23. theorem OAI.IsingPerceptron.enrichedContactObjective_exists_minimum line 405
  24. lemma OAI.IsingPerceptron.right_derivative_nonneg_of_min line 437
  25. def OAI.IsingPerceptron.enrichedFieldObjective line 446
  26. theorem OAI.IsingPerceptron.enriched_field_minimum_cone line 454
  27. lemma OAI.IsingPerceptron.finiteFieldPath_const_mul line 499
  28. lemma OAI.IsingPerceptron.enriched_contact_perturbation_minimum line 507
  29. lemma OAI.IsingPerceptron.enriched_contact_time_minimum line 522
  30. theorem OAI.IsingPerceptron.enriched_contact_cone line 539
  31. def OAI.IsingPerceptron.depthTail line 590
  32. lemma OAI.IsingPerceptron.continuous_depthTail line 591
  33. lemma OAI.IsingPerceptron.depthTail_mem line 596
  34. lemma OAI.IsingPerceptron.depthTail_level line 601
  35. lemma OAI.IsingPerceptron.finiteFieldPath_single line 606
  36. lemma OAI.IsingPerceptron.enrichedArrayLaw_depthTail line 616