OAI/Probability/IsingPerceptron/NormalizedRestrictionPi.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Normalized Restriction Pi.

  1. lemma OAI.IsingPerceptron.normalizedRestriction_pi line 15
  2. lemma OAI.IsingPerceptron.replica_restriction_mass_ne_zero line 31
  3. lemma OAI.IsingPerceptron.replica_restriction_eventually line 38
  4. def OAI.IsingPerceptron.subtypeReference line 44
  5. lemma OAI.IsingPerceptron.subtypeReference_preserving line 47
  6. lemma OAI.IsingPerceptron.subtypeReference_probability line 55
  7. lemma OAI.IsingPerceptron.referenceReplicaMean_subtype line 63
  8. lemma OAI.IsingPerceptron.cylinder_replica_law line 72
  9. lemma OAI.IsingPerceptron.cylinder_replica_variance_le line 80
  10. theorem OAI.IsingPerceptron.cylinder_replica_restriction_tendsto line 88
  11. theorem OAI.IsingPerceptron.cylinder_replica_insertion_restriction_tendsto line 112
  12. lemma OAI.IsingPerceptron.countable_reference_exhaustion line 148
  13. lemma OAI.IsingPerceptron.finite_restriction_cylinder_insertion line 172
  14. theorem OAI.IsingPerceptron.countable_cylinder_reference_insertion line 209
  15. lemma OAI.IsingPerceptron.measurable_countable_measure_pi line 256
  16. lemma OAI.IsingPerceptron.measurable_random_referencePartition line 272
  17. lemma OAI.IsingPerceptron.measurable_random_referenceReplicaMean line 282
  18. lemma OAI.IsingPerceptron.referenceReplicaMean_abs_le line 301
  19. lemma OAI.IsingPerceptron.integrable_of_measurable_abs_le line 311
  20. lemma OAI.IsingPerceptron.abs_integral_le_const_of_bound line 317
  21. lemma OAI.IsingPerceptron.measurable_random_cylinder_mean line 326
  22. lemma OAI.IsingPerceptron.integrable_random_cylinder_mean line 338
  23. theorem OAI.IsingPerceptron.random_countable_cylinder_insertion line 355
  24. lemma OAI.IsingPerceptron.joint_integrable_square_of_uniform_conditionals line 391
  25. lemma OAI.IsingPerceptron.measurable_random_cylinder_insertion line 407
  26. lemma OAI.IsingPerceptron.cylinder_replica_insertion_second line 424
  27. theorem OAI.IsingPerceptron.integrable_joint_cylinder_insertion line 453
  28. lemma OAI.IsingPerceptron.integrable_exp_of_integer_exp line 470
  29. lemma OAI.IsingPerceptron.random_cylinder_all_exp_ae line 486
  30. lemma OAI.IsingPerceptron.measurable_random_cylinder_cgf line 519
  31. lemma OAI.IsingPerceptron.cylinder_scaled_law line 529
  32. lemma OAI.IsingPerceptron.cylinder_cgf_second line 538
  33. lemma OAI.IsingPerceptron.integrable_random_cylinder_cgf line 553
  34. lemma OAI.IsingPerceptron.integrable_joint_cylinder_mean line 566
  35. theorem OAI.IsingPerceptron.joint_countable_cylinder_insertion line 577