Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,795 to 1,800 of 2,569 results.
oneJetBundle_model_space_chartAt
Mathematical statement
In the OneJetBundle to the model space, the charts are just the canonical identification between a product type and a bundle total space type, a.k.a. Bundle.TotalSpace.toProd.
Source project: Sphere eversion
Person-level attribution pending.
OpenSmoothEmbedding.contMDiff_update
Project documentation
This is lemma lem:smooth_updating in the blueprint.
Source project: Sphere eversion
Person-level attribution pending.
OpenSmoothEmbedding.dist_update
Mathematical statement
This is lem:dist_updating in the blueprint.
Source project: Sphere eversion
Person-level attribution pending.
operator_ineq_SSA
Mathematical statement
Operator extension of SSA (Main result of Lin-Kim-Hsieh). For positive definite ρ_AB and σ_BC: ρ_A⁻¹ ⊗ σ_BC ≤ ρ_AB⁻¹ ⊗ σ_C where ρ_A = Tr_B(ρ_AB) and σ_C = Tr_B(σ_BC), and the RHS is reindexed via the associator (dA × dB) × dC ≃ dA × (dB × dC).
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.exists_min
Mathematical statement
There exists an optimal T for the hypothesis testing, that is, it's a minimum and not just an infimum. This tightens the T from exists_min' to a ⟪ρ,T⟫ = 1 - ε bound.
Source project: quantumInfo
Person-level attribution pending.
OptimalHypothesisRate.exists_min'
Mathematical statement
There exists an optimal T for the hypothesis testing, that is, it's a minimum and not just an infimum. This states we have 1 - ε ≤ ρ.exp_val T, but we can always "worsen" T to make that bound tight, which is exists_min.
Source project: quantumInfo
Person-level attribution pending.