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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersQuantumMechanics.OneDimension.HilbertSpace.memHS_iff
Plain-language statement
A function f satisfies MemHS f if and only if it is almost everywhere strongly measurable, and square integrable.
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix
Project documentation
The tensor contrMetric is invariant under the action of LorentzGroup d. -/ @[simp] lemma actionT_contrMetric {d} (g : LorentzGroup d) : g • η d = η d := by erw [TensorSpecies.metricTensor_invariant] /- ## There value with respect to a basis
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.leviCivita_basis_repr_eq_zero_of_eq
Plain-language statement
The Levi-Civita tensor vanishes on any multi-index with a repeated value: if two distinct index positions i ≠ j carry the same basis index, the component is zero.
Source project: Physlib
Person-level attribution pending.
Reduction.id_perfectCompleteness
Plain-language statement
The identity / trivial reduction is perfectly complete.
Source project: ArkLib
Person-level attribution pending.
rightContinuous_integral_annulus
Plain-language statement
If is integrable on the open annulus , then varying the inner radius from the right changes the annular integral continuously at :
is right-continuous at .
Source project: Carleson formalization
Person-level attribution pending.
RigidBody.rho_coord_sub_centerOfMass
Plain-language statement
The first moment of the mass distribution about its own centre of mass vanishes: for nonzero mass, ρ of the centred j-th coordinate function is zero.
Source project: Physlib
Person-level attribution pending.