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,435 to 1,440 of 2,569 results.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_alghom_of_dvd_f
Mathematical statement
If Kn denotes the unramified extension of K of degree n, then Kn embeds into L if n ∣ f K L. This is half of the universal property.
Source project: Class Field Theory
Person-level attribution pending.
IsOpen.ae_eq_of_integral_contDiff_smul_eq
Project documentation
If ∫ ψ · f = ∫ ψ · g for all ψ ∈ Cc^∞(U), then f =ᵃᵉ g on U. This is the du Bois-Reymond lemma, the key uniqueness engine for weak derivatives.
Source project: PDE
Person-level attribution pending.
IsPerIndexQueryBound.toWorstCaseCostBound_unit_sum
Mathematical statement
If main makes at most qb i queries to each oracle i, then its total query count (under the unit cost model) is at most ∑ i, qb i on every execution path.
Source project: VCVio
Person-level attribution pending.
iSup_f_alpha_jointly_convex
Mathematical statement
Step 3 (Convexity in σ): For fixed H ≥ 0 and ρ, and α > 1, the map σ ↦ f_alpha α H ρ σ is convex. The key is that for p = α/(α−1) > 1: • A ↦ Tr[A^p] is convex on PSD matrices (trace function convexity, Theorem 2.10 of Carlen), • σ ↦ σ^{−γ} H σ^{−γ} is concave in σ by Lieb concavity (since −γ = (α−1)/(2α) ∈ (0,½)), • The composition...
Source project: quantumInfo
Person-level attribution pending.
iteratedDeriv_tanh_const_mul
Mathematical statement
Iterated derivative for scaled tanh
Source project: Physlib
Person-level attribution pending.
iteratedDeriv_tanh_is_polynomial_of_tanh
Mathematical statement
The nth derivative of Tanh(x) is a polynomial of Tanh(x)
Source project: Physlib
Person-level attribution pending.