OAI/Probability/SignedSweeps/ProvedRanges.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.weightedMoment_le_one_of_level_zero line 12
  2. theorem OAI.SignedSweeps.sparse_signed_occurrence_moment_bound line 19
  3. theorem OAI.SignedSweeps.signed_occurrence_moment_bound_proved_ranges line 34
  4. def OAI.SignedSweeps.finiteRegularRepresentation line 74
  5. lemma OAI.SignedSweeps.finiteRegularRepresentation_apply line 82
  6. def OAI.SignedSweeps.coefficientAction line 85
  7. lemma OAI.SignedSweeps.coefficientAction_apply line 89
  8. def OAI.SignedSweeps.conjugationSum line 93
  9. lemma OAI.SignedSweeps.conjugationSum_intertwines line 97
  10. lemma OAI.SignedSweeps.trace_conjugationSum line 110
  11. lemma OAI.SignedSweeps.conjugationSum_scalar line 118
  12. def OAI.SignedSweeps.matrixCoefficient line 140
  13. lemma OAI.SignedSweeps.matrixCoefficient_apply line 146
  14. lemma OAI.SignedSweeps.matrixCoefficient_intertwines line 150
  15. lemma OAI.SignedSweeps.matrixCoefficient_action line 156
  16. lemma OAI.SignedSweeps.matrixCoefficient_inner line 161
  17. def OAI.SignedSweeps.normalizedCoefficient line 179
  18. lemma OAI.SignedSweeps.normalizedCoefficient_inner line 182
  19. lemma OAI.SignedSweeps.normalizedCoefficient_action line 206
  20. lemma OAI.SignedSweeps.normalizedCoefficient_orthonormal line 211
  21. lemma OAI.SignedSweeps.positive_orthonormal_trace_le line 223
  22. lemma OAI.SignedSweeps.coefficientAction_positive line 236
  23. lemma OAI.SignedSweeps.irreducible_trace_le_regular line 256
  24. lemma OAI.SignedSweeps.finiteRegular_trace line 274
  25. def OAI.SignedSweeps.subgroupExtension line 284
  26. lemma OAI.SignedSweeps.subgroupExtension_apply line 291
  27. lemma OAI.SignedSweeps.subgroupExtension_apply_not_mem line 295
  28. lemma OAI.SignedSweeps.subgroup_sum_extension line 298
  29. lemma OAI.SignedSweeps.subgroupExtension_inner line 309
  30. lemma OAI.SignedSweeps.coefficientAction_subgroup line 319
  31. lemma OAI.SignedSweeps.subgroup_coefficient_compression line 339
  32. theorem OAI.SignedSweeps.subgroup_coefficient_positive line 349
  33. theorem OAI.SignedSweeps.subgroup_irreducible_trace_bound line 361
  34. def OAI.SignedSweeps.bilateralRepresentation line 384
  35. lemma OAI.SignedSweeps.bilateralRepresentation_apply line 394
  36. lemma OAI.SignedSweeps.bilateralRepresentation_norm line 399
  37. lemma OAI.SignedSweeps.bilateralRepresentation_left line 404
  38. lemma OAI.SignedSweeps.coefficientAction_right line 409
  39. def OAI.SignedSweeps.subgroupCoefficientCarrier line 419
  40. def OAI.SignedSweeps.subgroupCoefficientProjection line 434
  41. lemma OAI.SignedSweeps.subgroupCoefficientProjection_intertwines line 439
  42. lemma OAI.SignedSweeps.subgroupCoefficientProjection_commutes line 446
  43. lemma OAI.SignedSweeps.subgroupCoefficientProjection_symmetric line 460
  44. lemma OAI.SignedSweeps.subgroupCoefficientProjection_idempotent line 466
  45. lemma OAI.SignedSweeps.subgroupCoefficientProjection_fixes line 475
  46. lemma OAI.SignedSweeps.finiteRegular_coefficient_kernel line 483