Commit 2023-06-24 09:25 d2540561

View on Github →

feat: port Archive.Sensitivity (#5322)

Estimated changes

Modified Archive.lean

Created Archive/Sensitivity.lean

added theorem Sensitivity.Q.adj_iff_proj_adj

added theorem Sensitivity.Q.adj_iff_proj_eq

added theorem Sensitivity.Q.adjacent.symm

added def Sensitivity.Q.adjacent

added theorem Sensitivity.Q.card

added theorem Sensitivity.Q.ext

added theorem Sensitivity.Q.not_adjacent_zero

added theorem Sensitivity.Q.succ_n_eq

added def Sensitivity.Q

added theorem Sensitivity.V.ext

added def Sensitivity.V

added theorem Sensitivity.dim_V

added theorem Sensitivity.dualBases_e_ε

added theorem Sensitivity.duality

added theorem Sensitivity.e_zero_apply

added theorem Sensitivity.epsilon_total

added theorem Sensitivity.exists_eigenvalue

added theorem Sensitivity.f_image_g

added theorem Sensitivity.f_matrix

added theorem Sensitivity.f_squared

added theorem Sensitivity.f_succ_apply

added theorem Sensitivity.f_zero

added theorem Sensitivity.finrank_V

added theorem Sensitivity.g_apply

added theorem Sensitivity.g_injective

added theorem Sensitivity.huang_degree_theorem

added def Sensitivity.π