OAI/Combinatorics/Sidorenko/Normalization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.grassmannFactor line 12
  2. theorem OAI.SidorenkoCounterexample.grassmann_single_factor line 15
  3. theorem OAI.SidorenkoCounterexample.subspace_count_normalized line 25
  4. theorem OAI.SidorenkoCounterexample.inverse_power_tendsto_zero line 38
  5. theorem OAI.SidorenkoCounterexample.grassmannFactor_tendsto line 43
  6. theorem OAI.SidorenkoCounterexample.triangular_nat_add line 60
  7. theorem OAI.SidorenkoCounterexample.layerMass_normalized line 68
  8. theorem OAI.SidorenkoCounterexample.primeInfinity_real_tendsto line 80
  9. theorem OAI.SidorenkoCounterexample.symmetricSignProb_tendsto line 84
  10. theorem OAI.SidorenkoCounterexample.layerMass_tendsto line 97
  11. theorem OAI.SidorenkoCounterexample.maxOrthogonal_card_by_dimension line 122
  12. def OAI.SidorenkoCounterexample.orthogonalFactor line 142
  13. theorem OAI.SidorenkoCounterexample.choose_two_add line 145
  14. theorem OAI.SidorenkoCounterexample.maxOrthogonal_normalized line 151
  15. theorem OAI.SidorenkoCounterexample.orthogonalFactor_tendsto line 171
  16. theorem OAI.SidorenkoCounterexample.split_form_normalized line 196
  17. theorem OAI.SidorenkoCounterexample.signed_pair_compatibility line 219
  18. theorem OAI.SidorenkoCounterexample.signed_second_iff line 235
  19. theorem OAI.SidorenkoCounterexample.centerSubspaceEquiv_rank line 259
  20. theorem OAI.SidorenkoCounterexample.centerSubspaceEquiv_sign line 264
  21. def OAI.SidorenkoCounterexample.centerPredicateEquiv line 272
  22. def OAI.SidorenkoCounterexample.SignedProjector line 294
  23. def OAI.SidorenkoCounterexample.pairSignedCenterEquiv line 298
  24. def OAI.SidorenkoCounterexample.signedProjectorSubspaceEquiv line 317
  25. theorem OAI.SidorenkoCounterexample.restrict_eq_zero_iff_isotropic line 357
  26. theorem OAI.SidorenkoCounterexample.half_isotropic_iff_self line 371
  27. def OAI.SidorenkoCounterexample.halfIsotropicEquiv line 383
  28. def OAI.SidorenkoCounterexample.tripleSignedCenterEquiv line 396