OAI/Probability/IsingPerceptron/FieldChain.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Field Chain.

  1. def OAI.IsingPerceptron.chainPartition line 17
  2. def OAI.IsingPerceptron.chainFieldStep line 21
  3. def OAI.IsingPerceptron.chainExponent line 29
  4. lemma OAI.IsingPerceptron.chainExponent_apply line 32
  5. lemma OAI.IsingPerceptron.chainExponent_admissible line 35
  6. lemma OAI.IsingPerceptron.stepAt_chain line 49
  7. lemma OAI.IsingPerceptron.fieldRecursion_chain line 55
  8. lemma OAI.IsingPerceptron.jointPair_measurable line 105
  9. lemma OAI.IsingPerceptron.jointSpin_measurable line 107
  10. lemma OAI.IsingPerceptron.jointSpin_unit_support line 110
  11. lemma OAI.IsingPerceptron.joint_depthTail_quantile line 119
  12. def OAI.IsingPerceptron.finiteStepFunction line 185
  13. lemma OAI.IsingPerceptron.finite_cells_disjoint line 188
  14. lemma OAI.IsingPerceptron.measurable_finiteStepFunction line 199
  15. lemma OAI.IsingPerceptron.finiteStepFunction_on_cell line 206
  16. lemma OAI.IsingPerceptron.finiteStepFunction_mul line 216
  17. lemma OAI.IsingPerceptron.integral_finiteStepFunction line 230
  18. lemma OAI.IsingPerceptron.integral_finiteStepFunction_mul line 261
  19. lemma OAI.IsingPerceptron.finiteStep_tail_indicator line 280
  20. lemma OAI.IsingPerceptron.integral_finiteStep_tail line 314
  21. lemma OAI.IsingPerceptron.abs_linearGrowth line 334
  22. lemma OAI.IsingPerceptron.gaussian_abs_exp_bound line 338
  23. lemma OAI.IsingPerceptron.gaussianTransform_abs_bound line 375
  24. lemma OAI.IsingPerceptron.gaussianTransform_upper_abs line 392
  25. lemma OAI.IsingPerceptron.magneticRecursion_upper line 421
  26. lemma OAI.IsingPerceptron.magneticFieldValue_growth line 434
  27. lemma OAI.IsingPerceptron.finite_field_telescoping line 468
  28. lemma OAI.IsingPerceptron.field_sum_last_lower line 479
  29. def OAI.IsingPerceptron.chainWeight line 496
  30. lemma OAI.IsingPerceptron.chainWeight_pos line 498
  31. lemma OAI.IsingPerceptron.chain_field_telescoping line 501
  32. lemma OAI.IsingPerceptron.magneticFieldValue_chain_growth line 521
  33. lemma OAI.IsingPerceptron.contact_cone_depthTail line 543
  34. theorem OAI.IsingPerceptron.enriched_contact_nodal_tails line 564