OAI/Combinatorics/Sidorenko/Restrictions.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.uniformMean_swap line 13
  2. theorem OAI.SidorenkoCounterexample.uniformMean_translate line 22
  3. theorem OAI.SidorenkoCounterexample.uniformMean_average_translate line 25
  4. theorem OAI.SidorenkoCounterexample.rankOne_shift_error line 34
  5. theorem OAI.SidorenkoCounterexample.centered_formSign_abs line 50
  6. theorem OAI.SidorenkoCounterexample.equal_dimension_separating_dual line 58
  7. theorem OAI.SidorenkoCounterexample.rankOne_restrict line 81
  8. theorem OAI.SidorenkoCounterexample.rankOne_restrict_zero line 85
  9. theorem OAI.SidorenkoCounterexample.restriction_covariance_bound line 93
  10. theorem OAI.SidorenkoCounterexample.uniformMean_square line 164
  11. theorem OAI.SidorenkoCounterexample.uniformMean_abs_sq_le line 170
  12. theorem OAI.SidorenkoCounterexample.family_variance_bound line 175
  13. theorem OAI.SidorenkoCounterexample.restriction_family_variance line 214
  14. theorem OAI.SidorenkoCounterexample.restriction_family_L1_sq line 230
  15. abbrev OAI.SidorenkoCounterexample.AltForm line 250
  16. instance OAI.SidorenkoCounterexample.altForm_finite line 252
  17. def OAI.SidorenkoCounterexample.altFormToMap line 259
  18. theorem OAI.SidorenkoCounterexample.update_vec_zero line 271
  19. theorem OAI.SidorenkoCounterexample.update_vec_one line 275
  20. def OAI.SidorenkoCounterexample.mapToAltForm line 279
  21. def OAI.SidorenkoCounterexample.altFormMapEquiv line 296
  22. theorem OAI.SidorenkoCounterexample.altForm_card line 308
  23. def OAI.SidorenkoCounterexample.canonicalOrthogonal line 327
  24. theorem OAI.SidorenkoCounterexample.canonicalOrthogonal_apply line 348
  25. theorem OAI.SidorenkoCounterexample.canonicalOrthogonal_symm line 351
  26. theorem OAI.SidorenkoCounterexample.canonicalOrthogonal_nondegenerate line 356
  27. abbrev OAI.SidorenkoCounterexample.MaxOrthogonal line 376

    Source documentation

    MaxOrthogonals are self-orthogonal subspaces, equivalently isotropic subspaces of half the ambient dimension.

    abbrev MaxOrthogonal := {L : Submodule K (V × Module.Dual K V) //
…
  28. theorem OAI.SidorenkoCounterexample.maxOrthogonal_finrank line 379
  29. theorem OAI.SidorenkoCounterexample.formGraph_orthogonal_isotropic line 389
  30. def OAI.SidorenkoCounterexample.graphMaxOrthogonal line 401
  31. theorem OAI.SidorenkoCounterexample.graphMaxOrthogonal_form_injective line 408
  32. theorem OAI.SidorenkoCounterexample.maxOrthogonal_pairing_zero line 423
  33. theorem OAI.SidorenkoCounterexample.graphMaxOrthogonal_surjective line 429
  34. def OAI.SidorenkoCounterexample.maxOrthogonalGraphEquiv line 468
  35. theorem OAI.SidorenkoCounterexample.maxOrthogonal_card_sum line 483

    Source documentation

    Exact chart decomposition count: the vertical-annihilator stratum is retained rather than discarded as a negligible exceptional event.

     theorem maxOrthogonal_card_sum [Fintype K] [Finite V] (hK : ringChar K ≠ 2) :
    letI := Fintype.ofFinite (Submodule K V)
…
  36. theorem OAI.SidorenkoCounterexample.canonicalOrthogonal_matrix line 506
  37. theorem OAI.SidorenkoCounterexample.hyperbolic_block_det line 515
  38. theorem OAI.SidorenkoCounterexample.canonicalOrthogonal_sign line 528
  39. theorem OAI.SidorenkoCounterexample.split_form_equivalent line 535
  40. theorem OAI.SidorenkoCounterexample.split_form_card line 547