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 985 to 990 of 2,569 results.
Electromagnetism.ElectromagneticPotential.toFieldStrength_eval_eq_basis_repr
Mathematical statement
Evaluating both tensor indices of the field strength gives the coefficient in the standard tensor-product basis.
Source project: Physlib
Person-level attribution pending.
Electromagnetism.ElectromagneticPotential.toFieldStrength_ofGradient
Mathematical statement
A pure-gauge potential has vanishing field strength.
Source project: Physlib
Person-level attribution pending.
eLpNorm_czOperator_restrict_two_three_of_support_subset
Mathematical statement
The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]), uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is bounded by the sum of two operators which are both bounded: one is the convolution with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has a k...
Source project: Carleson formalization
Person-level attribution pending.
enforceOracle.fst_map_run_simulateQ
Mathematical statement
When the computation is within its query bound, enforcement is transparent: the output distribution is identical to running without enforcement.
Source project: VCVio
Person-level attribution pending.
enforceOracle.probEvent_counting_budget_eq
Mathematical statement
For a computation that is structurally within budget, the budget check in the counting semantics is redundant on the support.
Source project: VCVio
Person-level attribution pending.
Ensemble.mix_mEnsemble_pure_average
Mathematical statement
The average of f : MState d → T on an ensemble that mixes to a pure state ψ is f (pure ψ)
Source project: quantumInfo
Person-level attribution pending.