module module

`IndisputableMonolith.Quantum.PureTwoQubit.EntropyConcurrence`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.MasterTheorem module_import
IndisputableMonolith.Quantum module_import
IndisputableMonolith.Skeleton.Quantum module_import

declarations in this module (52)

def concurrence L71
theorem concurrence_nonneg L75
theorem concurrence_eq_zero_iff_det_zero L83
theorem concurrence_pos_iff_det_ne_zero L95
def frobeniusNormSq L106
def reducedDensity L116
theorem reducedDensity_trace_eq_frobenius L122
theorem reducedDensity_trace_eq_one_of_normalized L132
theorem reducedDensity_det_eq_normSq_det L145
theorem reducedDensity_det_eq_norm_det_sq L164
theorem reducedDensity_det_eq_concurrence_sq_div_four L173
theorem reducedDensity_det_ne_zero_of_concurrence_pos L183
theorem reducedDensity_discriminant_eq_one_sub_concurrence_sq L198
def lambdaPlus L211
def lambdaMinus L216
theorem lambdaPlus_add_lambdaMinus L220
theorem lambdaPlus_mul_lambdaMinus L227
theorem lambdaPair_sum_product_of_concurrence_unit_interval L238
def binaryEntropy L253
theorem binaryEntropy_zero_left L257
theorem binaryEntropy_zero_right L262
theorem binaryEntropy_symm L267
theorem binaryEntropy_pos_of_open_unit_interval L276
theorem inner_radius_lt_one_of_pos_concurrence L305
theorem inner_radius_in_unit_interval_of_pos_concurrence L329
theorem binaryEntropy_inner_radius_pos_of_concurrence L347
theorem reducedDensity_eq_mul_conjTranspose L358
theorem reducedDensity_isHermitian L365
theorem reducedDensity_trace_eq_frobenius_complex L372
theorem reducedDensity_trace_eq_one_of_normalized_complex L377
theorem lambdaPlus_sub_lambdaMinus L384
theorem lambdaPlus_ge_lambdaMinus L389
theorem sum_product_implies_quadratic L394
theorem eq_lambdaPlus_or_lambdaMinus_of_quadratic L401
theorem eigenvalues_fin_two_sum_eq_of_complex_sum L415
theorem eigenvalues_fin_two_prod_eq_of_complex_prod L421
theorem reducedDensity_eigenvalues_sum_eq_one L427
theorem reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four L437
theorem concurrence_sq_le_one_of_normalized L446
theorem concurrence_le_one_of_normalized L455
theorem reducedDensity_eigenvalues_eq_lambda_or_swap L462
def reducedDensityVonNeumannEntropy L485
theorem binaryEntropy_eq_neg_sum_lambda L490
def PureTwoQubitReducedEntropyTarget L504
theorem pureTwoQubitReducedEntropyTarget_holds L511
theorem pure_two_qubit_entropy_eq_binaryEntropy_inner_radius L536
abbrev PureTwoQubitReducedEntropyTargetDef L547
theorem pure_two_qubit_entropy_positive_of_concurrence_positive L557
theorem pure_two_qubit_entropy_positive_unconditional L571
structure PureTwoQubitConcurrenceEntropyCert L602
def pureTwoQubitConcurrenceEntropyCert L650
theorem pureTwoQubitConcurrenceEntropyCert_inhabited L665