-- WARNING: only add a result to this file if it is a significant result in physics, usually one
-- known by name, such as Gauss's law, Noether's theorem or the Bell inequality. Every other
-- result must be written with `lemma`, not `theorem`. Each result listed here must be written with
-- `theorem` and have a doc-string, and must be listed under the section of its library, by its
-- fully qualified name. `lake exe theorem_lint` checks this.

[Physlib]
ClassicalMechanics.euler_lagrange_varGradient
ClassicalMechanics.FreeParticle.linearMomentum_conserved
ClassicalMechanics.FreeParticle.kineticEnergy_conserved
ClassicalMechanics.hamiltons_equations_varGradient
ClassicalMechanics.deriv_comp_eq_poissonBracket
RigidBody.angularMomentum_eq_inertiaTensor_mulVec
RigidBodyMotion.velocity_eq_angularVelocity
RigidBody.inertiaTensorAbout_eq_centerOfMass_add_pointMass
RigidBody.rotationalKineticEnergy_eq_integral
RigidBodyMotion.kineticEnergy_eq_translational_add_rotational
RigidBodyMotion.kineticEnergy_eq_translational_add_angularVelocity
RigidBodyMotion.kineticEnergy_eq_translational_add_bodyAngularVelocity
ClassicalMechanics.planeWave_waveEquation
Electromagnetism.ThreeDimension.electricField_eq_3D
Electromagnetism.ThreeDimension.magneticField_eq_3D
Electromagnetism.ThreeDimension.gaussLawElectric
Electromagnetism.ThreeDimension.gaussLawMagnetic
Electromagnetism.ThreeDimension.ampereLaw
Electromagnetism.ThreeDimension.faradayLaw
FluidDynamics.CauchyFlow.matrixDiv_stress_eq_neg_grad_pressure_of_is_inviscid
FluidDynamics.navier_stokes_iff_convective_navier_stokes
FluidDynamics.euler_iff_convectiveEuler
Physlib.Wirtinger.dWirtingerDir_dWirtingerAntiDir_comm
Physlib.Wirtinger.dWirtingerCoord_dWirtingerAntiCoord_comm
Physlib.Wirtinger.differentiableAt_complex_iff_dWirtingerAntiDir_eq_zero
Physlib.Wirtinger.differentiableAt_complex_iff_dWirtingerAntiCoord_eq_zero
Matrix.diag_exp_of_blockTriangular_id
Matrix.det_exp
Matrix.det_exp_real
SM.SMNoGrav.One.accGravSatisfied
StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos
FieldSpecification.WickAlgebra.static_wick_theorem
FieldSpecification.wicks_theorem
FieldSpecification.WickAlgebra.wicks_theorem_normal_order
WickContraction.card_eq_cardFun
WickContraction.card_of_isfull_even
WickContraction.card_of_isfull_odd
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_completeness
LinearPMap.numericalRange_convex
LinearPMap.inner_map_polarization'
spaceTime.γ_anticomm
spaceTime.γ.ofCliffordAlgebra_surjective
Fermion.Dirac.gammaMatrix_anticomm
Fermion.Dirac.gamma_anticomm
lorentzAlgebra.exp_mem_lorentzGroup
lorentzAlgebra.exp_isProper
lorentzAlgebra.exp_isOrthochronous
lorentzAlgebra.exp_mem_restricted_lorentzGroup
LorentzGroup.exists_boost_mul_rotation
CanonicalEnsemble.thermodynamicEntropy_eq_shannonEntropy
CanonicalEnsemble.fluctuation_dissipation_theorem_finite
CanonicalEnsemble.helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy
CanonicalEnsemble.differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction
CanonicalEnsemble.meanEnergy_eq_neg_deriv_log_Z_of_beta
CanonicalEnsemble.energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq
CanonicalEnsemble.fluctuation_dissipation_energy_parametric
IdealGas.ideal_gas_law
MicroHamiltonian.entropy_A_eq_entropy_Z
MicroHamiltonian.β_eq_deriv_S_U
adiabatic_relation_log
adiabatic_relation_UaUbVaVb
UnitSystem.ext

[QuantumInfo]
CPTPMap.emulates_self
CPTPMap.emulates_trans
CPTPMap.εApproximates_self
CPTPMap.εApproximates_monotone
CPTPMap.achievesRate_0
CPTPMap.id_achievesRate_log_dim
CPTPMap.not_achievesRate_gt_log_dim_in
CPTPMap.not_achievesRate_gt_log_dim_out
CPTPMap.bddAbove_achievesRate
CPTPMap.zero_le_quantumCapacity
CPTPMap.quantumCapacity_ge_log_dim_in
CPTPMap.coherentInfo_le_quantumCapacity
CPTPMap.quantumCapacity_eq_piProd_coherentInfo
HPMap.funext_hermitian
HPMap.funext_pos
HPMap.funext_pos_trace
HPMap.funext_mstate
PMap.pos_Hermitian
PTPMap.pos_Hermitian
CPTPMap.ext
PUMap.pos_Hermitian
CPUMap.pos_Hermitian
CPTPMap.choi_ext
CPTPMap.choi_PSD_of_CPTP
CPTPMap.Tr_of_choi_of_CPTP
CPTPMap.compose_eq
CPTPMap.compose_assoc
CPTPMap.id_map
CPTPMap.id_MState
CPTPMap.id_compose
CPTPMap.compose_id
CPTPMap.replacement_apply
CPTPMap.eq_if_output_unique
CPTPMap.prod_apply_prod
CPTPMap.piProd_comp
CPTPMap.ofUnitary_eq_conj
CPTPMap.IsUnitary_iff_uConj
CPTPMap.purify_trace
CPTPMap.prep_append_map_entry
CPTPMap.choi_IsEmbedding
MatrixMap.Dual.trace_eq
MatrixMap.IsHermitianPreserving.dual
MatrixMap.IsPositive.dual
MatrixMap.dual_Unital
CPTPMap.dual.PTP_POVM
CPTPMap.exp_val_Dual
HPMap.inner_hermDual
HPMap.inner_hermDual'
MatrixMap.IsPositive.hermDual
HPMap.hermDual_Unital
PTPMap.hermDual.PTP_POVM
PTPMap.exp_val_hermDual
MatrixMap.map_choi_inv
MatrixMap.choi_map_inv
MatrixMap.choi_matrix_inj
MatrixMap.toMatrix_comp
MatrixMap.kron_def
MatrixMap.kron_comp_distrib
MatrixMap.kron_map_of_kron_state
MatrixMap.piProd_comp
pinching_sq_eq_self
pinching_kraus_ortho
pinching_bound
pinching_pythagoras
MatrixMap.IsTracePreserving_iff_trace_choi
MatrixMap.IsTracePreserving.apply_trace
MatrixMap.IsTracePreserving.trace_choi
MatrixMap.IsTracePreserving.comp
MatrixMap.IsTracePreserving.id
MatrixMap.IsTracePreserving.unit_linear
MatrixMap.IsTracePreserving.kron
MatrixMap.IsTracePreserving.piProd
MatrixMap.IsTracePreserving.of_kraus_isTracePreserving
MatrixMap.IsTracePreserving.submatrix
MatrixMap.Unital.id
MatrixMap.IsHermitianPreserving.id
MatrixMap.IsHermitianPreserving.comp
MatrixMap.IsPositive.comp
MatrixMap.IsPositive.id
MatrixMap.IsPositive.add
MatrixMap.IsPositive.smul
MatrixMap.IsCompletelyPositive.of_Fintype
MatrixMap.IsCompletelyPositive.comp
MatrixMap.IsCompletelyPositive.id
MatrixMap.IsCompletelyPositive.add
MatrixMap.IsCompletelyPositive.smul
MatrixMap.IsCompletelyPositive.zero
MatrixMap.IsCompletelyPositive.finset_sum
MatrixMap.kron_kronecker_const
MatrixMap.choi_PSD_iff_CP_map
MatrixMap.conj_isCompletelyPositive
MatrixMap.IsCompletelyPositive.submatrix
MatrixMap.of_kraus_isCompletelyPositive
MatrixMap.choi_of_kraus_R
MatrixMap.positive_subunital_norm_apply_le
MatrixMap.cp_subunital_opNorm_le_one
MatrixMap.kron_of_kraus
MatrixMap.IsCompletelyPositive.kron
MatrixMap.IsCompletelyPositive.piProd
ProbDistribution.nonempty
ProbDistribution.constant_of_exists_one
ProbDistribution.congr_symm_apply
ProbDistribution.fin_two_eq_coin
ProbDistribution.expect_val_eq_mixable_mix
ProbDistribution.expect_val_constant
ProbDistribution.zero_le_expect_val
ProbDistribution.expect_val_congr_eq_expect_val
H₁_nonneg
H₁_le_1
H₁_le_exp_m1
Hₛ_nonneg
Hₛ_le_log_d
Hₛ_constant_eq_zero
Hₛ_uniform
Hₛ_coin
sandwichedTraceFunctional_pos
sandwichedTraceFunctional_conj_unitary_MState
H_hat_conj_sigma
f_alpha_le_at_optimizer
traceFunctional_eq_iSup_f_alpha
f_alpha_convex_in_sigma
HermitianMat.ker_weighted_sum_le
sandwichedTraceFunctional_jointly_convex
sandwichedTraceFunctional_tensor_invariant
MState.conjTensorUnitary_M
sandwichedTraceFunctional_conj_tensorUnitary
sandwichedTraceFunctional_mono_traceRight
ker_le_traceRight
sandwichedRenyiEntropy_mono_traceRight
sandwichedRenyiEntropy_SWAP
sandwichedRenyiEntropy_mono_traceLeft
prep_append_eq_tensor_pure
sandwichedRenyiEntropy_DPI_gt_one
sandwichedRenyiEntropy_DPI
sandwichedRelRentropy_tendsto_qRelativeEnt
qRelativeEnt_joint_convexity
sandwichedRelRentropy.limit_at_one
sandwichedRelRentropy_additive_alpha_one
sandwichedRelRentropy_additive
qRelativeEnt_additive
sandwichedRelRentropy.continuousOn_Ioo_0_1
sandwichedRelRentropy.continuousAt_1
qRelativeEnt_ker
qRelativeEnt_ne_top_iff
qRelativeEnt_eq_top_iff
qRelativeEnt_relabel
qRelativeEnt_rank
qMutualInfo_as_qRelativeEnt
V_rho_isometry
V_sigma_isometry
Matrix.opNorm_mul_le
Matrix.opNorm_conjTranspose_eq_opNorm
W_mat_sq_le_one
intermediate_ineq
operator_ineq_SSA
Sᵥₙ_strong_subadditivity
Sᵥₙ_subadditivity
Sᵥₙ_pure_tripartite_triangle
Sᵥₙ_triangle_ineq_one_way
Sᵥₙ_triangle_subaddivity
Sᵥₙ_weak_monotonicity
qConditionalEnt_strong_subadditivity
qMutualInfo_strong_subadditivity
qcmi_nonneg
qcmi_le_2_log_dim
qcmi_le_2_log_dim'
Sᵥₙ_nonneg
Sᵥₙ_le_log_d
Sᵥₙ_of_pure_zero
Sᵥₙ_eq_trace_cfc_negMulLog
Sᵥₙ_relabel
Sᵥₙ_of_SWAP_eq
Sᵥₙ_of_assoc_eq
Sᵥₙ_of_assoc'_eq
Sᵥₙ_of_partial_eq
qConditionalEnt_of_pure_symm
qMutualInfo_symm
Sᵥₙ_pure_complement
analyticAt_complexLaplaceIntegrand
eventually_integrable_complexLaplaceIntegrand_of_mem_interior_convergenceDomain
analyticAt_complexLaplaceTransform_of_mem_interior_convergenceDomain
ContinuousLinearMap.support_eq_sup_eigenspace_nonzero
IsCompact.closure_continuous_sSup
IsCompact.closure_continuous_sInf
Bornology.IsBounded.continuous_sSup
Bornology.IsBounded.continuous_sInf
LinearMap.continuous_iSup
LinearMap.continuous_iInf
LinearMap.continuous_iSup'
LinearMap.continuous_iInf'
LinearMap.BilinForm.continuous_iSup
LinearMap.BilinForm.continuous_iInf
ContinuousLinearMap.continuous_iSup
GeneralizedPerspectiveFunction.theorem_2_6_forward_jointlyConcaveOn_psd_pd
GeneralizedPerspectiveFunction.theorem_2_6_forward_jointlyConcaveOn_psd_pd_Ici
JensenOperatorInequality.nontrivial_hsumL_wrap
JensenOperatorInequality.theorem_2_5_2_i_all_imp_v
JensenOperatorInequalityScratch.nontrivial_hsumL
OperatorGeometricMean.operatorPowerMean_jointlyConcaveOn_pdSet
OperatorGeometricMean.operatorPowerMean_jointlyConvexOn_pdSet
HermitianMat.H
HermitianMat.ker_eq_eigenspace_zero
HermitianMat.support_eq_sup_eigenspace_nonzero
HermitianMat.kron_commute
HermitianMat.kron_id_commute_id_kro
Matrix.range_mul_conjTranspose_of_ker_le_ker
HermitianMat.spectrum_rcLike
HermitianMat.cfc_congr_of_nonneg
HermitianMat.cfc_congr_of_posDef
HermitianMat.cfc_reindex
HermitianMat.cfc_toMat_eq_sum_smul_proj
HermitianMat.mat_cfc_mul
HermitianMat.cfc_nonneg_of_nonneg
HermitianMat.continuous_cfc_fun
HermitianMat.continuousOn_cfc_fun
HermitianMat.continuousOn_cfc_fun_nonsingular
HermitianMat.continuousOn_cfc_fun_nonneg
HermitianMat.continuousOn_cfc_fun_posDef
Commute.exists_HermitianMat_cfc
HermitianMat.cfc_le_cfc_of_commute
HermitianMat.inner_eq_trace_mul
HermitianMat.inner_eq_trace_trivial
HermitianMat.inner_ge_zero
HermitianMat.inner_le_mul_trace
HermitianMat.inner_zero_iff
HermitianMat.unitInterval_IsCompact
Commute.exp_left'
Commute.exp_right'
HermitianMat.exp_nonneg
HermitianMat.exp_pos
HermitianMat.logApprox_mono
HermitianMat.logApprox_eq_cfc_scalar
HermitianMat.logApprox_eq_log_add_error
HermitianMat.log_mono
HermitianMat.le_of_exp_commute
HermitianMat.logApprox_concave
HermitianMat.log_concave
HermitianMat.log_kron
HermitianMat.kronecker_nonneg
HermitianMat.kronecker_self_mono
HermitianMat.kronecker_pos
HermitianMat.conj_nonneg
HermitianMat.le_smul_one_imp_eigenvalues_le
HermitianMat.eigenvalues_le_imp_le_smul_one
HermitianMat.eigenvalues_nonneg
HermitianMat.mat_nonneg
HermitianMat.mat_pos
Matrix.nonneg_conjTranspose_mul_self
Matrix.nonneg_self_mul_conjTranspose
HermitianMat.peierls_inequality
HermitianMat.trace_function_convex_univ
HermitianMat.trace_function_convex_ici
HermitianMat.projector_eq_sum_rankOne
HermitianMat.posPart_eq_posPart_toMat
HermitianMat.negPart_eq_negPart_toMat
HermitianMat.posPart_eq_cfc_lt
HermitianMat.negPart_eq_cfc_lt
HermitianMat.nonneg_iff_inner_nonneg
HermitianMat.continuousOn_rpow_pos
HermitianMat.continuousOn_rpow_neg
HermitianMat.reindex_rpow
HermitianMat.continuousOn_rpow_joint_nonneg_pos
HermitianMat.cfc_sq_rpow_eq_cfc_rpow
HermitianMat.rpow_le_rpow_of_posDef
HermitianMat.rpow_le_rpow_of_le
HermitianMat.trace_eq_trace
HermitianMat.trace_eq_trace_trivial
HermitianMat.trace_eq_trace_rc
HermitianMat.eigenvalues_conj
Matrix.IsHermitian.cfc_eq_any_isometry
Matrix.IsHermitian.cfc_eq_any_unitary
LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace'
iSup_mono_bot
LinearMap.IsSymmetric.directSum_isInternal_of_commute'
Matrix.SharedEigenbasis.sharedEigenvectorUnitary_mulVec
Matrix.SharedEigenbasis.mulVec_sharedEigenbasisA
Matrix.SharedEigenbasis.star_shared_mul_B_mul_IsDiag
Matrix.IsDiag.exists_cfc
Commute.exists_cfc
Filter.tendsto_sub_atTop_iff_nat
ENNReal.tendsto_sub_const_nhds_zero_iff
Matrix.fromBlocks_gram_posSemidef
Matrix.IsHermitian.sum_eigenvalues_eq_trace
Matrix.IsHermitian.eigenvalues_zero_eq_zero
Matrix.PosSemidef.stdBasisMatrix_iff_eq
Matrix.trace_mul_kron_one_right
Matrix.trace_mul_one_kron_right
Matrix.traceRight_eq_traceLeft_reindex
Matrix.traceNorm_neg
Matrix.traceNorm_isometry_left
Matrix.traceNorm_isometry_right
Matrix.traceNorm_unitary_conj
Matrix.traceNorm_Hermitian_eq_sum_abs_eigenvalues
Matrix.traceNorm_nonneg
Matrix.traceNorm_zero_iff
Matrix.traceNorm_smul
Matrix.exists_svd_sqrt_eigenvalues
Matrix.traceNorm_eq_sum_singularValues
Matrix.traceNorm_eq_sum_singularValuesSorted
Matrix.singularValues_le_opNorm
Matrix.traceNorm_mul_le_opNorm_traceNorm
Matrix.traceNorm_conjTranspose
Matrix.traceNorm_mul_le_traceNorm_opNorm
Matrix.traceNorm_sandwich_le
Matrix.abs_trace_le_traceNorm
Matrix.traceNorm_eq_max_re_tr_U
Matrix.traceNorm_add_le
Matrix.PosSemidef.traceNorm_eq_trace
Matrix.traceNorm_convex
minimax
LinearMap.BilinForm.minimax
LinearMap.BilinForm.minimax'
ciSup_ciInf_le_ciInf_ciSup
sion_minimax
Superadditive.tendsto_lim
LinearMap.IsSymmetric.conj_unitary_IsSymmetric
POVM.traceLeft_measurementMap_eq_measure
MState.uConj_spectrum_eq
MState.no_cloning
ResourcePretheory.prodRelabel_relabel_cast_prod
FreeStateTheory.IsCompact_IsFree
UnitalFreeStateTheory.RelativeEntResource.tendsto
UnitalFreeStateTheory.RelativeEntResource.tendsto_ennreal
OptimalHypothesisRate.iInf_IsCompact
OptimalHypothesisRate.iInf_IsConvex
OptimalHypothesisRate.of_empty
OptimalHypothesisRate.exists_min'
OptimalHypothesisRate.exists_min
OptimalHypothesisRate.pos_of_lt_one
OptimalHypothesisRate.optimalHypothesisRate_antitone
OptimalHypothesisRate.Ref81Lem5
OptimalHypothesisRate.optimalHypothesisRate_unique
SteinsLemma.Lemma6
SteinsLemma.LemmaS3_inf
SteinsLemma.log_le_f
SteinsLemma.f_le_log
SteinsLemma.Lemma7
SteinsLemma.Lemma7_gap
SteinsLemma.GeneralizedQSteinsLemma
SteinsLemma.limit_hypotesting_eq_limit_rel_entropy
Ensemble.coe_PEnsemble_iff_pure_states
Ensemble.mix_congrMEnsemble_eq_mix
Ensemble.mix_congrPEnsemble_eq_mix
Ensemble.average_of_pure_ensemble
Ensemble.mix_pEnsemble_pure_average
Ensemble.mix_mEnsemble_pure_average
Ensemble.trivial_mEnsemble_mix
Ensemble.trivial_mEnsemble_average
Ensemble.trivial_pEnsemble_mix
Ensemble.trivial_pEnsemble_average
Ensemble.spectral_ensemble_mix
convex_roof_ne_top
mixed_convex_roof_ne_top
mixed_convex_roof_le_convex_roof
convex_roof_of_pure
mixed_convex_roof_of_pure
EoF_of_MES
MState.fidelity_self_eq_one
MState.fidelity_eq_traceNorm_sqrt_mul_sqrt
MState.fidelity_eq_one_iff_self
MState.fidelity_symm
MState.fidelity_channel_nondecreasing
MState.Hermitian
MState.m_inj
MState.convex
MState.exp_val_eq_zero_iff
MState.exp_val_eq_one_iff
MState.spectrum_pure_eq_constant
MState.pure_of_constant_spectrum
MState.pure_iff_constant_spectrum
MState.pure_prod_pure
MState.traceLeft_prod_eq
MState.traceRight_prod_eq
MState.spectrum_prod
MState.IsSeparable_prod
MState.PhaseEquiv_iff_pure_eq
MState.pure_separable_iff_IsProd
MState.pure_iff_rank_eq_one
MState.Ket.IsProd_iff_rank_eq_one
MState.pure_separable_iff_traceLeft_pure
MState.purify_spec
MState.relabel_pure_exists
MState.purity_relabel
MState.toMat_IsEmbedding
MState.PosDef_mix
MState.PosDef_mix_of_ne_zero
MState.PosDef_mix_of_ne_one
TrDistance.symm
TrDistance.eq_abs_eigenvalues
Ket.normalize_ket_eq_self
Braket.dot_self_eq_one
Ket.IsProd_prod
Ket.not_IsEntangled_prod
Ket.IsProd_iff_mul_eq_mul
Ket.MES_isEntangled
transposeTrick
Qubit.X_Y_anticomm
Qubit.Y_Z_anticomm
Qubit.Z_X_anticomm

[PhyslibAlpha]
ClassicalFieldTheory.Local.isCritical_iff_eulerLagrange_zero
Electromagnetism.ThreeDimension.continuityEquation
Electromagnetism.TempDistElectromagneticPotential.continuityEquation
LinearMap.lie_apply_eq_of_lie_basis_eq
LinearMap.lie_apply_eq_of_lie_span_eq
LadderSystem.lie_E
LadderSystem.lie_totalN_E
LadderSystem.vacuumSpan_eq_of_ne_bot
LadderSystem.linearIndependent_word_countFun
LadderSystem.finrank_vacuumSpan_eq_choose
QuadraticMap.toMultilinearMap_continuous
QuadraticMap.toMultilinearMapHalfPolarBilin_continuous
QuadraticMap.toContinuousMultilinearMap_apply
QuadraticMap.toContinuousMultilinearMap_applyHalf
le_of_littleO
isLocalMin_of_posDef_of_littleo
second_derivative_test
second_derivative_test_analyticAt
QuantumMechanics.HarmonicOscillator.loweringCLM_vacuumGaussian
QuantumMechanics.HarmonicOscillator.hasVacuum_vacuumGaussian
stinespringOp_apply
complCard
Ud_orthonormal₁
Ud_orthonormal₂
unitary_of_orthonormal
tracefree_version
heisenberg_schrõdinger
unitaryForm_of_general
unitaryForm_of_general_e
stinespringOp_gram
stinespringForm_eq
