OAI/Probability/IsingPerceptron/EnrichedGGFinite.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Enriched G G Finite.

  1. def OAI.IsingPerceptron.enrichedMonomialResidual line 16
  2. lemma OAI.IsingPerceptron.enrichedMonomialResidual_bound line 28
  3. def OAI.IsingPerceptron.enrichedPerturbationObjective line 67
  4. lemma OAI.IsingPerceptron.enriched_minimum_coordinate line 73
  5. def OAI.IsingPerceptron.newReplicaEmbedding line 114
  6. lemma OAI.IsingPerceptron.newReplicaEmbedding_injective line 117
  7. lemma OAI.IsingPerceptron.sum_nonzero_permutation line 140
  8. lemma OAI.IsingPerceptron.jointEntry_monomial_le line 147
  9. def OAI.IsingPerceptron.monomialPair line 155
  10. lemma OAI.IsingPerceptron.abs_monomialPair_le_one line 158
  11. def OAI.IsingPerceptron.finiteJointBlock line 161
  12. def OAI.IsingPerceptron.permutedBlockTest line 164
  13. lemma OAI.IsingPerceptron.enrichedArrayLawTest_integral line 168
  14. lemma OAI.IsingPerceptron.permutedBlockTest_embedding line 185
  15. lemma OAI.IsingPerceptron.enrichedArrayLaw_residual line 194
  16. lemma OAI.IsingPerceptron.jointMonomialResidual_zero line 288
  17. lemma OAI.IsingPerceptron.enrichedArrayLaw_residual_bound line 297
  18. theorem OAI.IsingPerceptron.enriched_minimizers_jointGG line 327