Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

sorry count #3

Open
12 of 19 tasks
jjaassoonn opened this issue Oct 5, 2022 · 1 comment
Open
12 of 19 tasks

sorry count #3

jjaassoonn opened this issue Oct 5, 2022 · 1 comment

Comments

@jjaassoonn
Copy link
Collaborator

jjaassoonn commented Oct 5, 2022 •
edited
Loading

Now it is just 5 sorry!

  • to_anaysis/inner_product_space/tensor_product.lean: sorry free
  • to_anaysis/inner_product_space/tensor_power.lean: sorry free
  • combinatorics/simple_graph/cyclic: sorry free
  • combinatorics/simple_graph/independent: 1 sorry left
  • combinatorics/simple_graph/independent: 3 sorry left
    • independence_number_le_lovasz_number_at: probably needs to prove orthonormal sets can be extends to orthonormal basis.
    • real.Sup_mul_Sup (supremum of the pointwise product of two sets is the products of their supremum) done in e7b6401
    • pow_lovasz_number_at done in 3ec0df2
  • combinatorics/simple_graph/shannon_capacity: sorry free
  • combinatorics/simple_graph/strong_product: sorry free
  • linear_algebra/tensor_power: sorry free
  • five_cycles: 5 sorry
    • lovasz_umbrella.to_fun
    • lovasz_umbrella.norm_eq_one': should follow from lovasz_umbrella.to_fun
    • inner_eq_zero_of_ne_of_not_adj': should follow from lovasz_umbrella.to_fun
    • inner_lovasz_umbrella_e₁: should follow from lovasz_umbrella.to_fun
    • lovasz_number_at_lovasz_umbrella_eq finished in 1d35361
    • le_shannon_capacity_cyclic_graph_five reduced tostrong_pow_two_independence_number :5 ≤ (⊠^2 (cyclic 5)).independence_number in 483f91a, finished in 379e26c.

1 sorry (independence_number_le_lovasz_number_at) is a linear algebra problem. 4 sorries are about constructing the lovasz_umbrella.
@ocfnash
Copy link
Owner

ocfnash commented Oct 6, 2022

Thanks @jjaassoonn !

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ocfnash @jjaassoonn